New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqcom | Unicode version |
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom 191 | . . 3 | |
2 | 1 | albii 1566 | . 2 |
3 | dfcleq 2347 | . 2 | |
4 | dfcleq 2347 | . 2 | |
5 | 2, 3, 4 | 3bitr4i 268 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wal 1540 wceq 1642 wcel 1710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-cleq 2346 |
This theorem is referenced by: eqcoms 2356 eqcomi 2357 eqcomd 2358 eqeq2 2362 eqtr2 2371 eqtr3 2372 abeq1 2459 pm13.181 2589 necom 2597 gencbvex 2901 reu7 3031 eqsbc3r 3103 dfss 3260 sspsstri 3371 dfss5 3461 disj4 3599 ssnelpss 3613 preqr1 4124 snelpw1 4146 0nel1c 4159 eluni1g 4172 opkelopkabg 4245 otkelins2kg 4253 otkelins3kg 4254 opkelcokg 4261 opksnelsik 4265 iota1 4353 sniota 4369 0nelsuc 4400 nndisjeq 4429 preaddccan2lem1 4454 0cnelphi 4597 copsex4g 4610 opeqexb 4620 br1stg 4730 setconslem1 4731 opelxp 4811 elxp3 4831 brswap2 4860 dmopab3 4917 rncoeq 4975 xpcan 5057 xpcan2 5058 dmsnn0 5064 dffn5 5363 fnrnfv 5364 fvelrnb 5365 dfimafn2 5367 funimass4 5368 fnsnfv 5373 dmfco 5381 fnasrn 5417 dffo4 5423 fconstfv 5456 fvclss 5462 funiunfv 5467 dff13 5471 isomin 5496 f1oiso 5499 opbr1st 5501 opbr2nd 5502 oprabid 5550 eloprabga 5578 ovelimab 5610 brsnsi 5773 brsnsi1 5775 brsnsi2 5776 brco1st 5777 brco2nd 5778 txpcofun 5803 otsnelsi3 5805 brcupg 5814 fnsex 5832 qrpprod 5836 dmpprod 5840 fnpprod 5843 brcrossg 5848 pw1fnex 5852 brpw1fn 5854 dfnnc3 5885 antisymex 5912 erth2 5969 qsid 5990 mapexi 6003 xpassenlem 6056 xpassen 6057 enmap2lem1 6063 enmap2lem3 6065 enmap1lem1 6069 nenpw1pwlem1 6084 ncseqnc 6128 leltctr 6212 taddc 6229 letc 6231 ce0lenc1 6239 brtcfn 6246 ncfin 6247 csucex 6259 addccan2nclem1 6263 nncdiv3lem1 6275 nncdiv3lem2 6276 nnc3n3p1 6278 nnc3n3p2 6279 spacvallem1 6281 nchoicelem1 6289 nchoicelem2 6290 nchoicelem16 6304 |
Copyright terms: Public domain | W3C validator |