Theorem eqcom 2179

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 140	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1470	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2171	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2171	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 212	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 105   A.wal 1351   = wceq 1353   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqcoms  2180  eqcomi  2181  neqcomd  2182  eqcomd  2183  eqeq2  2187  eqtr2  2196  eqtr3  2197  abeq1  2287  nesym  2392  pm13.181  2429  necom  2431  gencbvex  2784  gencbval  2786  clel5  2875  eqsbc2  3024  dfss  3144  dfss5  3341  rabrsndc  3661  preqr1g  3767  preqr1  3769  invdisj  3998  opthg2  4240  copsex4g  4248  opcom  4251  opeqsn  4253  opeqpr  4254  reusv3  4461  suc11g  4557  opthprc  4678  elxp3  4681  relop  4778  dmopab3  4841  rncoeq  4901  restidsing  4964  dfrel4v  5081  dmsnm  5095  iota1  5193  sniota  5208  dffn5im  5562  fvelrnb  5564  dfimafn2  5566  funimass4  5567  fnsnfv  5576  dmfco  5585  fndmdif  5622  fneqeql  5625  rexrn  5654  ralrn  5655  elrnrexdmb  5657  dffo4  5665  ftpg  5701  fconstfvm  5735  foima2  5753  rexima  5756  ralima  5757  dff13  5769  f1eqcocnv  5792  eusvobj2  5861  f1ocnvfv3  5864  oprabid  5907  eloprabga  5962  ovelimab  6025  dfoprab3  6192  f1o2ndf1  6229  cnvoprab  6235  brtpos2  6252  tpossym  6277  frecsuclem  6407  nntri3or  6494  erth2  6580  brecop  6625  erovlem  6627  ecopovsym  6631  ecopovsymg  6634  xpcomco  6826  mapen  6846  nneneq  6857  supelti  7001  djuf1olem  7052  eldju  7067  omp1eomlem  7093  nninfwlporlemd  7170  exmidontriimlem3  7222  ordpipqqs  7373  addcanprg  7615  ltsrprg  7746  caucvgsrlemcl  7788  caucvgsrlemfv  7790  elreal  7827  ltresr  7838  axcaucvglemcl  7894  axcaucvglemval  7896  addsubeq4  8172  subcan2  8182  negcon1  8209  negcon2  8210  addid0  8330  divmulap2  8633  conjmulap  8686  rerecclap  8687  creur  8916  creui  8917  nndiv  8960  elznn0  9268  zltnle  9299  uzm1  9558  divfnzn  9621  zq  9626  icoshftf1o  9991  iccf1o  10004  fzen  10043  fzneuz  10101  4fvwrd4  10140  qltnle  10246  flqeqceilz  10318  modq0  10329  modqmuladdnn0  10368  addmodlteq  10398  nn0ennn  10433  uzennn  10436  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  seq3f1olemstep  10501  exp3val  10522  qsqeqor  10631  hashfacen  10816  cjreb  10875  caucvgrelemrec  10988  minmax  11238  xrnegiso  11270  xrnegcon1d  11272  xrminmax  11273  pwm1geoserap1  11516  dvdsval2  11797  dvdsabseq  11853  dvdsflip  11857  odd2np1  11878  oddm1even  11880  sqoddm1div8z  11891  m1exp1  11906  divalgb  11930  modremain  11934  zeqzmulgcd  11971  dfgcd2  12015  divgcdcoprm0  12101  prm2orodd  12126  hashdvds  12221  oddprmdvds  12352  oddennn  12393  evenennn  12394  grpid  12912  grpinvcnv  12938  grplmulf1o  12944  grpsubeq0  12956  grpsubadd  12958  grplactcnv  12972  isnsg4  13072  dvdsr02  13274  01eq0ring  13330  rmodislmodlem  13440  toponsspwpwg  13525  dmtopon  13526  hmeoimaf1o  13817  txhmeo  13822  limcmpted  14135  ioocosf1o  14278  lgseisenlem2  14454  2lgsoddprmlem2  14457  bj-peano4  14710  pwle2  14751  subctctexmid  14753  pw1nct  14755  exmidsbthrlem  14773  iooref1o  14785  iswomni0  14802