Theorem eqcom 2195

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 1481	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2187	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2187	. 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 1362   = wceq 1364   e. wcel 2164

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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  eqcoms  2196  eqcomi  2197  neqcomd  2198  eqcomd  2199  eqeq2  2203  eqtr2  2212  eqtr3  2213  abeq1  2303  nesym  2409  pm13.181  2446  necom  2448  gencbvex  2806  gencbval  2808  clel5  2897  eqsbc2  3046  dfss  3167  dfss5  3364  rabrsndc  3686  preqr1g  3792  preqr1  3794  invdisj  4023  opthg2  4268  copsex4g  4276  opcom  4279  opeqsn  4281  opeqpr  4282  reusv3  4491  suc11g  4589  opthprc  4710  elxp3  4713  relop  4812  dmopab3  4875  rncoeq  4935  restidsing  4998  dfrel4v  5117  dmsnm  5131  iota1  5229  sniota  5245  dffn5im  5602  fvelrnb  5604  dfimafn2  5606  funimass4  5607  fnsnfv  5616  dmfco  5625  fndmdif  5663  fneqeql  5666  rexrn  5695  ralrn  5696  elrnrexdmb  5698  dffo4  5706  ftpg  5742  fconstfvm  5776  foima2  5794  rexima  5797  ralima  5798  dff13  5811  f1eqcocnv  5834  eusvobj2  5904  f1ocnvfv3  5907  oprabid  5950  eloprabga  6005  ovelimab  6069  dfoprab3  6244  f1o2ndf1  6281  cnvoprab  6287  brtpos2  6304  tpossym  6329  frecsuclem  6459  nntri3or  6546  erth2  6634  brecop  6679  erovlem  6681  ecopovsym  6685  ecopovsymg  6688  xpcomco  6880  mapen  6902  nneneq  6913  supelti  7061  djuf1olem  7112  eldju  7127  omp1eomlem  7153  nninfwlporlemd  7231  exmidontriimlem3  7283  ordpipqqs  7434  addcanprg  7676  ltsrprg  7807  caucvgsrlemcl  7849  caucvgsrlemfv  7851  elreal  7888  ltresr  7899  axcaucvglemcl  7955  axcaucvglemval  7957  addsubeq4  8234  subcan2  8244  negcon1  8271  negcon2  8272  addid0  8392  divmulap2  8695  conjmulap  8748  rerecclap  8749  creur  8978  creui  8979  nndiv  9023  elznn0  9332  zltnle  9363  uzm1  9623  divfnzn  9686  zq  9691  icoshftf1o  10057  iccf1o  10070  fzen  10109  fzneuz  10167  4fvwrd4  10206  qltnle  10313  flqeqceilz  10389  modq0  10400  modqmuladdnn0  10439  addmodlteq  10469  nn0ennn  10504  uzennn  10507  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  seq3f1olemstep  10585  exp3val  10612  qsqeqor  10721  hashfacen  10907  cjreb  11010  caucvgrelemrec  11123  minmax  11373  xrnegiso  11405  xrnegcon1d  11407  xrminmax  11408  pwm1geoserap1  11651  dvdsval2  11933  dvdsabseq  11989  dvdsflip  11993  odd2np1  12014  oddm1even  12016  sqoddm1div8z  12027  m1exp1  12042  divalgb  12066  modremain  12070  zeqzmulgcd  12107  dfgcd2  12151  divgcdcoprm0  12239  prm2orodd  12264  hashdvds  12359  oddprmdvds  12492  oddennn  12549  evenennn  12550  gsumval2  12980  grpid  13111  grpinvcnv  13140  grplmulf1o  13146  grpsubeq0  13158  grpsubadd  13160  grplactcnv  13174  isnsg4  13282  eqg0el  13299  conjghm  13346  conjnmzb  13350  dvdsr02  13601  01eq0ring  13685  rmodislmodlem  13846  rspsn  14030  zndvds  14137  znleval  14141  toponsspwpwg  14190  dmtopon  14191  hmeoimaf1o  14482  txhmeo  14487  limcmpted  14817  ioocosf1o  14989  gausslemma2dlem0i  15173  lgseisenlem2  15187  2lgsoddprmlem2  15194  bj-peano4  15447  pwle2  15489  subctctexmid  15491  pw1nct  15493  exmidsbthrlem  15512  iooref1o  15524  iswomni0  15541