![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqcom | GIF version |
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqcom | ⊢ (A = B ↔ B = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom 128 | . . 3 ⊢ ((x ∈ A ↔ x ∈ B) ↔ (x ∈ B ↔ x ∈ A)) | |
2 | 1 | albii 1356 | . 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ ∀x(x ∈ B ↔ x ∈ A)) |
3 | dfcleq 2031 | . 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
4 | dfcleq 2031 | . 2 ⊢ (B = A ↔ ∀x(x ∈ B ↔ x ∈ A)) | |
5 | 2, 3, 4 | 3bitr4i 201 | 1 ⊢ (A = B ↔ B = A) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1240 = wceq 1242 ∈ wcel 1390 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: eqcoms 2040 eqcomi 2041 eqcomd 2042 eqeq2 2046 eqtr2 2055 eqtr3 2056 abeq1 2144 nesym 2244 pm13.181 2281 necom 2283 gencbvex 2594 gencbval 2596 eqsbc3r 2813 dfss 2926 dfss5 3136 disj4im 3270 ssnelpss 3283 rabrsndc 3429 preqr1g 3528 preqr1 3530 invdisj 3750 opthg2 3967 copsex4g 3975 opcom 3978 opeqsn 3980 opeqpr 3981 reusv3 4158 suc11g 4235 dtruex 4237 opthprc 4334 elxp3 4337 relop 4429 dmopab3 4491 rncoeq 4548 dfrel4v 4715 dmsnm 4729 iota1 4824 sniota 4837 dffn5im 5162 fvelrnb 5164 dfimafn2 5166 funimass4 5167 fnsnfv 5175 dmfco 5184 fndmdif 5215 fneqeql 5218 rexrn 5247 ralrn 5248 elrnrexdmb 5250 dffo4 5258 ftpg 5290 fconstfvm 5322 rexima 5337 ralima 5338 dff13 5350 f1eqcocnv 5374 eusvobj2 5441 f1ocnvfv3 5444 oprabid 5480 eloprabga 5533 ovelimab 5593 dfoprab3 5759 f1o2ndf1 5791 brtpos2 5807 tpossym 5832 frecsuclem3 5929 nntri3or 6011 erth2 6087 brecop 6132 erovlem 6134 ecopovsym 6138 ecopovsymg 6141 xpcomco 6236 ordpipqqs 6358 addcanprg 6590 ltsrprg 6675 elreal 6727 ltresr 6736 addsubeq4 7023 subcan2 7032 negcon1 7059 negcon2 7060 divmulap2 7437 conjmulap 7487 rerecclap 7488 creur 7692 creui 7693 nndiv 7735 elznn0 8036 zltnle 8067 uzm1 8279 divfnzn 8332 zq 8337 icoshftf1o 8629 iccf1o 8642 fzen 8677 fzneuz 8733 4fvwrd4 8767 nn0ennn 8890 cjreb 9094 bj-peano4 9415 |
Copyright terms: Public domain | W3C validator |