Theorem eqcom 2207

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 1493	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2199	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2199	. 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 1371   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ext 2187

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

This theorem is referenced by:  eqcoms  2208  eqcomi  2209  neqcomd  2210  eqcomd  2211  eqeq2  2215  eqtr2  2224  eqtr3  2225  abeq1  2315  nesym  2421  pm13.181  2458  necom  2460  gencbvex  2819  gencbval  2821  clel5  2910  eqsbc2  3059  dfss  3180  dfss5  3378  rabrsndc  3701  preqr1g  3807  preqr1  3809  invdisj  4038  opthg2  4284  copsex4g  4292  opcom  4296  opeqsn  4298  opeqpr  4299  reusv3  4508  suc11g  4606  opthprc  4727  elxp3  4730  relop  4829  dmopab3  4892  rncoeq  4953  restidsing  5016  dfrel4v  5135  dmsnm  5149  iota1  5247  sniota  5263  dffn5im  5626  fvelrnb  5628  dfimafn2  5630  funimass4  5631  fnsnfv  5640  dmfco  5649  fndmdif  5687  fneqeql  5690  rexrn  5719  ralrn  5720  elrnrexdmb  5722  dffo4  5730  ftpg  5770  fconstfvm  5804  foima2  5822  rexima  5825  ralima  5826  dff13  5839  f1eqcocnv  5862  eusvobj2  5932  f1ocnvfv3  5935  oprabid  5978  eloprabga  6034  ovelimab  6099  dfoprab3  6279  f1o2ndf1  6316  cnvoprab  6322  brtpos2  6339  tpossym  6364  frecsuclem  6494  nntri3or  6581  erth2  6669  brecop  6714  erovlem  6716  ecopovsym  6720  ecopovsymg  6723  xpcomco  6923  mapen  6945  nneneq  6956  supelti  7106  djuf1olem  7157  eldju  7172  omp1eomlem  7198  nninfwlporlemd  7276  exmidontriimlem3  7337  ordpipqqs  7489  addcanprg  7731  ltsrprg  7862  caucvgsrlemcl  7904  caucvgsrlemfv  7906  elreal  7943  ltresr  7954  axcaucvglemcl  8010  axcaucvglemval  8012  addsubeq4  8289  subcan2  8299  negcon1  8326  negcon2  8327  addid0  8447  divmulap2  8751  conjmulap  8804  rerecclap  8805  creur  9034  creui  9035  nndiv  9079  elznn0  9389  zltnle  9420  uzm1  9681  divfnzn  9744  zq  9749  icoshftf1o  10115  iccf1o  10128  fzen  10167  fzneuz  10225  4fvwrd4  10264  qltnle  10388  flqeqceilz  10465  modq0  10476  modqmuladdnn0  10515  addmodlteq  10545  nn0ennn  10580  uzennn  10583  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemab  10649  seq3f1olemstep  10661  exp3val  10688  qsqeqor  10797  hashfacen  10983  cjreb  11210  caucvgrelemrec  11323  minmax  11574  xrnegiso  11606  xrnegcon1d  11608  xrminmax  11609  pwm1geoserap1  11852  dvdsval2  12134  dvdsabseq  12191  dvdsflip  12195  odd2np1  12217  oddm1even  12219  sqoddm1div8z  12230  m1exp1  12245  divalgb  12269  modremain  12273  zeqzmulgcd  12324  dfgcd2  12368  divgcdcoprm0  12456  prm2orodd  12481  hashdvds  12576  oddprmdvds  12710  oddennn  12796  evenennn  12797  gsumval2  13262  grpid  13404  grpinvcnv  13433  grplmulf1o  13439  grpsubeq0  13451  grpsubadd  13453  grplactcnv  13467  isnsg4  13581  eqg0el  13598  conjghm  13645  conjnmzb  13649  dvdsr02  13900  01eq0ring  13984  rmodislmodlem  14145  rspsn  14329  zndvds  14444  znleval  14448  psr1clfi  14483  toponsspwpwg  14527  dmtopon  14528  hmeoimaf1o  14819  txhmeo  14824  limcmpted  15168  ioocosf1o  15359  fsumdvdsmul  15496  gausslemma2dlem0i  15567  lgseisenlem2  15581  lgsquadlem2  15588  2lgslem1c  15600  2lgsoddprmlem2  15616  2lgsoddprm  15623  bj-peano4  15928  pwle2  15972  subctctexmid  15974  pw1nct  15977  exmidsbthrlem  15998  iooref1o  16010  iswomni0  16027