Theorem eqcom 2084

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqcom	|- ( A = B <-> B = A )

Proof of Theorem eqcom

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 138	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1400	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2076	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2076	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 210	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 103   A.wal 1283   = wceq 1285   e. wcel 1434

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