Theorem eqcom 2231

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 1516	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2223	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2223	. 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 1393   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqcoms  2232  eqcomi  2233  neqcomd  2234  eqcomd  2235  eqeq2  2239  eqtr2  2248  eqtr3  2249  abeq1  2339  nesym  2445  pm13.181  2482  necom  2484  gencbvex  2847  gencbval  2849  clel5  2940  eqsbc2  3089  dfss  3211  dfss5  3409  rabrsndc  3734  preqr1g  3844  preqr1  3846  invdisj  4076  opthg2  4325  copsex4g  4333  opcom  4337  opeqsn  4339  opeqpr  4340  reusv3  4551  suc11g  4649  opthprc  4770  elxp3  4773  relop  4872  dmopab3  4936  rncoeq  4998  restidsing  5061  dfrel4v  5180  dmsnm  5194  iota1  5293  sniota  5309  dffn5im  5679  fvelrnb  5681  dfimafn2  5683  funimass4  5684  fnsnfv  5693  dmfco  5702  fndmdif  5740  fneqeql  5743  rexrn  5772  ralrn  5773  elrnrexdmb  5775  dffo4  5783  ftpg  5823  fconstfvm  5857  foima2  5875  rexima  5878  ralima  5879  dff13  5892  f1eqcocnv  5915  riotaeqimp  5979  eusvobj2  5987  f1ocnvfv3  5990  oprabid  6033  eloprabga  6091  ovelimab  6156  dfoprab3  6337  f1o2ndf1  6374  cnvoprab  6380  brtpos2  6397  tpossym  6422  frecsuclem  6552  nntri3or  6639  erth2  6727  brecop  6772  erovlem  6774  ecopovsym  6778  ecopovsymg  6781  xpcomco  6985  mapen  7007  nneneq  7018  supelti  7169  djuf1olem  7220  eldju  7235  omp1eomlem  7261  nninfwlporlemd  7339  exmidontriimlem3  7405  ordpipqqs  7561  addcanprg  7803  ltsrprg  7934  caucvgsrlemcl  7976  caucvgsrlemfv  7978  elreal  8015  ltresr  8026  axcaucvglemcl  8082  axcaucvglemval  8084  addsubeq4  8361  subcan2  8371  negcon1  8398  negcon2  8399  addid0  8519  divmulap2  8823  conjmulap  8876  rerecclap  8877  creur  9106  creui  9107  nndiv  9151  elznn0  9461  zltnle  9492  uzm1  9753  divfnzn  9816  zq  9821  icoshftf1o  10187  iccf1o  10200  fzen  10239  fzneuz  10297  4fvwrd4  10336  qltnle  10463  flqeqceilz  10540  modq0  10551  modqmuladdnn0  10590  addmodlteq  10620  nn0ennn  10655  uzennn  10658  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  seq3f1olemstep  10736  exp3val  10763  qsqeqor  10872  hashfacen  11058  wrd2ind  11255  cjreb  11377  caucvgrelemrec  11490  minmax  11741  xrnegiso  11773  xrnegcon1d  11775  xrminmax  11776  pwm1geoserap1  12019  dvdsval2  12301  dvdsabseq  12358  dvdsflip  12362  odd2np1  12384  oddm1even  12386  sqoddm1div8z  12397  m1exp1  12412  divalgb  12436  modremain  12440  zeqzmulgcd  12491  dfgcd2  12535  divgcdcoprm0  12623  prm2orodd  12648  hashdvds  12743  oddprmdvds  12877  oddennn  12963  evenennn  12964  gsumval2  13430  grpid  13572  grpinvcnv  13601  grplmulf1o  13607  grpsubeq0  13619  grpsubadd  13621  grplactcnv  13635  isnsg4  13749  eqg0el  13766  conjghm  13813  conjnmzb  13817  dvdsr02  14069  01eq0ring  14153  rmodislmodlem  14314  rspsn  14498  zndvds  14613  znleval  14617  psr1clfi  14652  toponsspwpwg  14696  dmtopon  14697  hmeoimaf1o  14988  txhmeo  14993  limcmpted  15337  ioocosf1o  15528  fsumdvdsmul  15665  gausslemma2dlem0i  15736  lgseisenlem2  15750  lgsquadlem2  15757  2lgslem1c  15769  2lgsoddprmlem2  15785  2lgsoddprm  15792  uspgredgiedg  15976  uspgriedgedg  15977  uspgr2wlkeq  16076  wlk0prc  16083  wlklenvclwlk  16084  bj-peano4  16318  pwle2  16364  subctctexmid  16366  pw1nct  16369  exmidsbthrlem  16390  iooref1o  16402  iswomni0  16419