Theorem eqcom 2233

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 1518	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2225	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2225	. 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 1395   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  eqcoms  2234  eqcomi  2235  neqcomd  2236  eqcomd  2237  eqeq2  2241  eqtr2  2250  eqtr3  2251  abeq1  2341  nesym  2447  pm13.181  2484  necom  2486  gencbvex  2850  gencbval  2852  clel5  2943  eqsbc2  3092  dfss  3214  dfss5  3412  rabrsndc  3739  preqr1g  3849  preqr1  3851  invdisj  4081  opthg2  4331  copsex4g  4339  opcom  4343  opeqsn  4345  opeqpr  4346  reusv3  4557  suc11g  4655  opthprc  4777  elxp3  4780  relop  4880  dmopab3  4944  rncoeq  5006  restidsing  5069  dfrel4v  5188  dmsnm  5202  iota1  5301  sniota  5317  dffn5im  5691  fvelrnb  5693  dfimafn2  5695  funimass4  5696  fnsnfv  5705  dmfco  5714  fndmdif  5752  fneqeql  5755  rexrn  5784  ralrn  5785  elrnrexdmb  5787  dffo4  5795  ftpg  5838  fconstfvm  5872  foima2  5892  rexima  5895  ralima  5896  dff13  5909  f1eqcocnv  5932  riotaeqimp  5996  eusvobj2  6004  f1ocnvfv3  6007  oprabid  6050  eloprabga  6108  ovelimab  6173  dfoprab3  6354  f1o2ndf1  6393  cnvoprab  6399  brtpos2  6417  tpossym  6442  frecsuclem  6572  nntri3or  6661  erth2  6749  brecop  6794  erovlem  6796  ecopovsym  6800  ecopovsymg  6803  xpcomco  7010  mapen  7032  nneneq  7043  supelti  7201  djuf1olem  7252  eldju  7267  omp1eomlem  7293  nninfwlporlemd  7371  exmidontriimlem3  7438  ordpipqqs  7594  addcanprg  7836  ltsrprg  7967  caucvgsrlemcl  8009  caucvgsrlemfv  8011  elreal  8048  ltresr  8059  axcaucvglemcl  8115  axcaucvglemval  8117  addsubeq4  8394  subcan2  8404  negcon1  8431  negcon2  8432  addid0  8552  divmulap2  8856  conjmulap  8909  rerecclap  8910  creur  9139  creui  9140  nndiv  9184  elznn0  9494  zltnle  9525  uzm1  9787  divfnzn  9855  zq  9860  icoshftf1o  10226  iccf1o  10239  fzen  10278  fzneuz  10336  4fvwrd4  10375  qltnle  10504  flqeqceilz  10581  modq0  10592  modqmuladdnn0  10631  addmodlteq  10661  nn0ennn  10696  uzennn  10699  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  seq3f1olemstep  10777  exp3val  10804  qsqeqor  10913  hashfacen  11101  wrd2ind  11308  cjreb  11444  caucvgrelemrec  11557  minmax  11808  xrnegiso  11840  xrnegcon1d  11842  xrminmax  11843  pwm1geoserap1  12087  dvdsval2  12369  dvdsabseq  12426  dvdsflip  12430  odd2np1  12452  oddm1even  12454  sqoddm1div8z  12465  m1exp1  12480  divalgb  12504  modremain  12508  zeqzmulgcd  12559  dfgcd2  12603  divgcdcoprm0  12691  prm2orodd  12716  hashdvds  12811  oddprmdvds  12945  oddennn  13031  evenennn  13032  gsumval2  13498  grpid  13640  grpinvcnv  13669  grplmulf1o  13675  grpsubeq0  13687  grpsubadd  13689  grplactcnv  13703  isnsg4  13817  eqg0el  13834  conjghm  13881  conjnmzb  13885  dvdsr02  14138  01eq0ring  14222  rmodislmodlem  14383  rspsn  14567  zndvds  14682  znleval  14686  psr1clfi  14721  toponsspwpwg  14765  dmtopon  14766  hmeoimaf1o  15057  txhmeo  15062  limcmpted  15406  ioocosf1o  15597  fsumdvdsmul  15734  gausslemma2dlem0i  15805  lgseisenlem2  15819  lgsquadlem2  15826  2lgslem1c  15838  2lgsoddprmlem2  15854  2lgsoddprm  15861  uspgredgiedg  16048  uspgriedgedg  16049  uspgr2wlkeq  16235  wlk0prc  16242  wlklenvclwlk  16243  eupth2lem2dc  16329  bj-peano4  16601  pwle2  16650  subctctexmid  16652  pw1nct  16655  exmidsbthrlem  16677  iooref1o  16689  iswomni0  16707