Theorem eqcom 2083

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 1399	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2075	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2075	. 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 1282   = wceq 1284   e. wcel 1433

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 1376  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  eqcoms  2084  eqcomi  2085  eqcomd  2086  eqeq2  2090  eqtr2  2099  eqtr3  2100  abeq1  2188  nesym  2290  pm13.181  2327  necom  2329  gencbvex  2645  gencbval  2647  eqsbc3r  2874  dfss  2987  dfss5  3171  rabrsndc  3460  preqr1g  3558  preqr1  3560  invdisj  3780  opthg2  3994  copsex4g  4002  opcom  4005  opeqsn  4007  opeqpr  4008  reusv3  4210  suc11g  4300  opthprc  4409  elxp3  4412  relop  4504  dmopab3  4566  rncoeq  4623  dfrel4v  4792  dmsnm  4806  iota1  4901  sniota  4914  dffn5im  5240  fvelrnb  5242  dfimafn2  5244  funimass4  5245  fnsnfv  5253  dmfco  5262  fndmdif  5293  fneqeql  5296  rexrn  5325  ralrn  5326  elrnrexdmb  5328  dffo4  5336  ftpg  5368  fconstfvm  5400  rexima  5415  ralima  5416  dff13  5428  f1eqcocnv  5451  eusvobj2  5518  f1ocnvfv3  5521  oprabid  5557  eloprabga  5611  ovelimab  5671  dfoprab3  5837  f1o2ndf1  5869  cnvoprab  5875  brtpos2  5889  tpossym  5914  frecsuclem3  6013  nntri3or  6095  erth2  6174  brecop  6219  erovlem  6221  ecopovsym  6225  ecopovsymg  6228  xpcomco  6323  nneneq  6343  supelti  6415  ordpipqqs  6564  addcanprg  6806  ltsrprg  6924  caucvgsrlemcl  6965  caucvgsrlemfv  6967  elreal  6997  ltresr  7007  axcaucvglemcl  7061  axcaucvglemval  7063  addsubeq4  7323  subcan2  7333  negcon1  7360  negcon2  7361  addid0  7477  divmulap2  7764  conjmulap  7817  rerecclap  7818  creur  8036  creui  8037  nndiv  8079  elznn0  8366  zltnle  8397  uzm1  8649  divfnzn  8706  zq  8711  icoshftf1o  9013  iccf1o  9026  fzen  9062  fzneuz  9118  4fvwrd4  9150  qltnle  9255  flqeqceilz  9320  modq0  9331  modqmuladdnn0  9370  addmodlteq  9400  nn0ennn  9425  cjreb  9753  caucvgrelemrec  9865  minmax  10112  dvdsval2  10198  dvdsabseq  10247  dvdsflip  10251  odd2np1  10272  oddm1even  10274  sqoddm1div8z  10286  m1exp1  10301  divalgb  10325  modremain  10329  zeqzmulgcd  10362  dfgcd2  10403  divgcdcoprm0  10483  prm2orodd  10508  bj-peano4  10750