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 | ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bicom 128 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴)) | |
2 | 1 | albii 1359 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴)) |
3 | dfcleq 2034 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
4 | dfcleq 2034 | . 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴)) | |
5 | 2, 3, 4 | 3bitr4i 201 | 1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∀wal 1241 = wceq 1243 ∈ wcel 1393 |
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 1336 ax-gen 1338 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqcoms 2043 eqcomi 2044 eqcomd 2045 eqeq2 2049 eqtr2 2058 eqtr3 2059 abeq1 2147 nesym 2250 pm13.181 2287 necom 2289 gencbvex 2600 gencbval 2602 eqsbc3r 2819 dfss 2932 dfss5 3142 disj4im 3276 ssnelpss 3289 rabrsndc 3438 preqr1g 3537 preqr1 3539 invdisj 3759 opthg2 3976 copsex4g 3984 opcom 3987 opeqsn 3989 opeqpr 3990 reusv3 4192 suc11g 4281 dtruex 4283 opthprc 4391 elxp3 4394 relop 4486 dmopab3 4548 rncoeq 4605 dfrel4v 4772 dmsnm 4786 iota1 4881 sniota 4894 dffn5im 5219 fvelrnb 5221 dfimafn2 5223 funimass4 5224 fnsnfv 5232 dmfco 5241 fndmdif 5272 fneqeql 5275 rexrn 5304 ralrn 5305 elrnrexdmb 5307 dffo4 5315 ftpg 5347 fconstfvm 5379 rexima 5394 ralima 5395 dff13 5407 f1eqcocnv 5431 eusvobj2 5498 f1ocnvfv3 5501 oprabid 5537 eloprabga 5591 ovelimab 5651 dfoprab3 5817 f1o2ndf1 5849 brtpos2 5866 tpossym 5891 frecsuclem3 5990 nntri3or 6072 erth2 6151 brecop 6196 erovlem 6198 ecopovsym 6202 ecopovsymg 6205 xpcomco 6300 nneneq 6320 ordpipqqs 6472 addcanprg 6714 ltsrprg 6832 caucvgsrlemcl 6873 caucvgsrlemfv 6875 elreal 6905 ltresr 6915 axcaucvglemcl 6969 axcaucvglemval 6971 addsubeq4 7226 subcan2 7236 negcon1 7263 negcon2 7264 divmulap2 7655 conjmulap 7705 rerecclap 7706 creur 7911 creui 7912 nndiv 7954 elznn0 8260 zltnle 8291 uzm1 8503 divfnzn 8556 zq 8561 icoshftf1o 8859 iccf1o 8872 fzen 8907 fzneuz 8963 4fvwrd4 8997 qltnle 9101 flqeqceilz 9160 modq0 9171 nn0ennn 9209 cjreb 9466 caucvgrelemrec 9578 bj-peano4 10080 |
Copyright terms: Public domain | W3C validator |