Theorem eqcom 2156

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 139	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1447	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2148	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2148	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 211	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 104   A.wal 1330   = wceq 1332   e. wcel 2125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147

This theorem is referenced by:  eqcoms  2157  eqcomi  2158  neqcomd  2159  eqcomd  2160  eqeq2  2164  eqtr2  2173  eqtr3  2174  abeq1  2264  nesym  2369  pm13.181  2406  necom  2408  gencbvex  2755  gencbval  2757  eqsbc3r  2993  dfss  3112  dfss5  3308  rabrsndc  3623  preqr1g  3725  preqr1  3727  invdisj  3955  opthg2  4194  copsex4g  4202  opcom  4205  opeqsn  4207  opeqpr  4208  reusv3  4414  suc11g  4510  opthprc  4630  elxp3  4633  relop  4729  dmopab3  4792  rncoeq  4852  dfrel4v  5030  dmsnm  5044  iota1  5142  sniota  5155  dffn5im  5507  fvelrnb  5509  dfimafn2  5511  funimass4  5512  fnsnfv  5520  dmfco  5529  fndmdif  5565  fneqeql  5568  rexrn  5597  ralrn  5598  elrnrexdmb  5600  dffo4  5608  ftpg  5644  fconstfvm  5678  foima2  5693  rexima  5696  ralima  5697  dff13  5709  f1eqcocnv  5732  eusvobj2  5800  f1ocnvfv3  5803  oprabid  5843  eloprabga  5898  ovelimab  5961  dfoprab3  6129  f1o2ndf1  6165  cnvoprab  6171  brtpos2  6188  tpossym  6213  frecsuclem  6343  nntri3or  6429  erth2  6514  brecop  6559  erovlem  6561  ecopovsym  6565  ecopovsymg  6568  xpcomco  6760  mapen  6780  nneneq  6791  supelti  6934  djuf1olem  6983  eldju  6998  omp1eomlem  7024  exmidontriimlem3  7137  ordpipqqs  7273  addcanprg  7515  ltsrprg  7646  caucvgsrlemcl  7688  caucvgsrlemfv  7690  elreal  7727  ltresr  7738  axcaucvglemcl  7794  axcaucvglemval  7796  addsubeq4  8069  subcan2  8079  negcon1  8106  negcon2  8107  addid0  8227  divmulap2  8528  conjmulap  8581  rerecclap  8582  creur  8809  creui  8810  nndiv  8853  elznn0  9161  zltnle  9192  uzm1  9448  divfnzn  9508  zq  9513  icoshftf1o  9873  iccf1o  9886  fzen  9923  fzneuz  9981  4fvwrd4  10017  qltnle  10123  flqeqceilz  10195  modq0  10206  modqmuladdnn0  10245  addmodlteq  10275  nn0ennn  10310  uzennn  10313  iseqf1olemqcl  10363  iseqf1olemnab  10365  iseqf1olemab  10366  seq3f1olemstep  10378  exp3val  10399  hashfacen  10684  cjreb  10743  caucvgrelemrec  10856  minmax  11106  xrnegiso  11136  xrnegcon1d  11138  xrminmax  11139  pwm1geoserap1  11382  dvdsval2  11663  dvdsabseq  11712  dvdsflip  11716  odd2np1  11737  oddm1even  11739  sqoddm1div8z  11750  m1exp1  11765  divalgb  11789  modremain  11793  zeqzmulgcd  11826  dfgcd2  11869  divgcdcoprm0  11949  prm2orodd  11974  hashdvds  12064  oddennn  12072  evenennn  12073  toponsspwpwg  12359  dmtopon  12360  hmeoimaf1o  12653  txhmeo  12658  limcmpted  12971  ioocosf1o  13114  bj-peano4  13468  pwle2  13509  subctctexmid  13512  pw1nct  13514  exmidsbthrlem  13534  iooref1o  13546  iswomni0  13563