Skip to content

Commit

Permalink
comment update
Browse files Browse the repository at this point in the history
  • Loading branch information
GinoGiotto committed Jan 25, 2024
1 parent d338b17 commit 1fb94b9
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -46709,7 +46709,8 @@ although the definition does not require it (see ~ dfid2 for a case
$( Change first bound variable in an ordered-pair class abstraction, using
explicit substitution. (Contributed by NM, 6-Oct-2004.) (Revised by
Mario Carneiro, 14-Oct-2016.) Add disjoint variable condition to avoid
~ ax-13 . (Revised by Gino Giotto, 17-Jan-2024.) $)
~ ax-13 . See ~ cbvopab1g for a less restrictive version requiring more
axioms. (Revised by Gino Giotto, 17-Jan-2024.) $)
cbvopab1 $p |- { <. x , y >. | ph } = { <. z , y >. | ps } $=
( vw vv cv cop wceq wa wex cab copab nfv nfan nfex wsb nfs1v opeq1 eqeq2d
sbequ12 anbi12d exbidv cbvexv1 nfsbv sbhypf bitri abbii df-opab 3eqtr4i )
Expand Down

0 comments on commit 1fb94b9

Please sign in to comment.