![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 138 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | albii 1400 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfcleq 2076 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfcleq 2076 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4i 210 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-cleq 2075 |
This theorem is referenced by: eqcoms 2085 eqcomi 2086 eqcomd 2087 eqeq2 2091 eqtr2 2100 eqtr3 2101 abeq1 2189 nesym 2291 pm13.181 2328 necom 2330 gencbvex 2646 gencbval 2648 eqsbc3r 2875 dfss 2988 dfss5 3178 rabrsndc 3468 preqr1g 3566 preqr1 3568 invdisj 3788 opthg2 4002 copsex4g 4010 opcom 4013 opeqsn 4015 opeqpr 4016 reusv3 4218 suc11g 4308 opthprc 4417 elxp3 4420 relop 4514 dmopab3 4576 rncoeq 4633 dfrel4v 4802 dmsnm 4816 iota1 4911 sniota 4924 dffn5im 5251 fvelrnb 5253 dfimafn2 5255 funimass4 5256 fnsnfv 5264 dmfco 5273 fndmdif 5304 fneqeql 5307 rexrn 5336 ralrn 5337 elrnrexdmb 5339 dffo4 5347 ftpg 5379 fconstfvm 5411 rexima 5426 ralima 5427 dff13 5439 f1eqcocnv 5462 eusvobj2 5529 f1ocnvfv3 5532 oprabid 5568 eloprabga 5622 ovelimab 5682 dfoprab3 5848 f1o2ndf1 5880 cnvoprab 5886 brtpos2 5900 tpossym 5925 frecsuclem 6055 nntri3or 6137 erth2 6217 brecop 6262 erovlem 6264 ecopovsym 6268 ecopovsymg 6271 xpcomco 6370 nneneq 6392 supelti 6474 ordpipqqs 6626 addcanprg 6868 ltsrprg 6986 caucvgsrlemcl 7027 caucvgsrlemfv 7029 elreal 7059 ltresr 7069 axcaucvglemcl 7123 axcaucvglemval 7125 addsubeq4 7390 subcan2 7400 negcon1 7427 negcon2 7428 addid0 7544 divmulap2 7831 conjmulap 7884 rerecclap 7885 creur 8103 creui 8104 nndiv 8146 elznn0 8447 zltnle 8478 uzm1 8730 divfnzn 8787 zq 8792 icoshftf1o 9089 iccf1o 9102 fzen 9138 fzneuz 9194 4fvwrd4 9227 qltnle 9332 flqeqceilz 9400 modq0 9411 modqmuladdnn0 9450 addmodlteq 9480 nn0ennn 9515 cjreb 9891 caucvgrelemrec 10003 minmax 10250 dvdsval2 10343 dvdsabseq 10392 dvdsflip 10396 odd2np1 10417 oddm1even 10419 sqoddm1div8z 10430 m1exp1 10445 divalgb 10469 modremain 10473 zeqzmulgcd 10506 dfgcd2 10547 divgcdcoprm0 10627 prm2orodd 10652 oddennn 10730 evenennn 10731 bj-peano4 10935 |
Copyright terms: Public domain | W3C validator |