![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > eqcom | Structured version 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 1339 | . 2 ⊢ (∀x(x ∈ A ↔ x ∈ B) ↔ ∀x(x ∈ B ↔ x ∈ A)) |
3 | dfcleq 2017 | . 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
4 | dfcleq 2017 | . 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 1226 = wceq 1228 ∈ wcel 1375 |
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 1316 ax-gen 1318 ax-ext 2005 |
This theorem depends on definitions: df-bi 110 df-cleq 2016 |
This theorem is referenced by: eqcoms 2026 eqcomi 2027 eqcomd 2028 eqeq2 2032 eqtr2 2041 eqtr3 2042 abeq1 2130 nesym 2227 pm13.181 2264 necom 2266 gencbvex 2576 gencbval 2578 eqsbc3r 2795 dfss 2908 dfss5 3118 disj4im 3252 ssnelpss 3265 rabrsndc 3411 preqr1g 3510 preqr1 3512 invdisj 3732 opthg2 3949 copsex4g 3957 opcom 3960 opeqsn 3962 opeqpr 3963 reusv3 4140 suc11g 4217 dtruex 4219 opthprc 4316 elxp3 4319 relop 4411 dmopab3 4473 rncoeq 4530 dfrel4v 4697 dmsnm 4711 iota1 4806 sniota 4819 dffn5im 5142 fvelrnb 5144 dfimafn2 5146 funimass4 5147 fnsnfv 5155 dmfco 5164 fndmdif 5195 fneqeql 5198 rexrn 5227 ralrn 5228 elrnrexdmb 5230 dffo4 5238 ftpg 5270 fconstfvm 5302 rexima 5317 ralima 5318 dff13 5330 f1eqcocnv 5354 eusvobj2 5420 f1ocnvfv3 5423 oprabid 5459 eloprabga 5512 ovelimab 5572 dfoprab3 5737 f1o2ndf1 5769 brtpos2 5785 tpossym 5810 frec0g 5897 frecsuclem3 5901 nntri3or 5982 erth2 6056 brecop 6100 erovlem 6102 ecopovsym 6106 ecopovsymg 6109 ordpipqqs 6225 bj-peano4 6522 |
Copyright terms: Public domain | W3C validator |