Theorem eqcom 2198

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 1484	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2190	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2190	. 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 2167

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  eqcoms  2199  eqcomi  2200  neqcomd  2201  eqcomd  2202  eqeq2  2206  eqtr2  2215  eqtr3  2216  abeq1  2306  nesym  2412  pm13.181  2449  necom  2451  gencbvex  2810  gencbval  2812  clel5  2901  eqsbc2  3050  dfss  3171  dfss5  3368  rabrsndc  3690  preqr1g  3796  preqr1  3798  invdisj  4027  opthg2  4272  copsex4g  4280  opcom  4283  opeqsn  4285  opeqpr  4286  reusv3  4495  suc11g  4593  opthprc  4714  elxp3  4717  relop  4816  dmopab3  4879  rncoeq  4939  restidsing  5002  dfrel4v  5121  dmsnm  5135  iota1  5233  sniota  5249  dffn5im  5606  fvelrnb  5608  dfimafn2  5610  funimass4  5611  fnsnfv  5620  dmfco  5629  fndmdif  5667  fneqeql  5670  rexrn  5699  ralrn  5700  elrnrexdmb  5702  dffo4  5710  ftpg  5746  fconstfvm  5780  foima2  5798  rexima  5801  ralima  5802  dff13  5815  f1eqcocnv  5838  eusvobj2  5908  f1ocnvfv3  5911  oprabid  5954  eloprabga  6009  ovelimab  6074  dfoprab3  6249  f1o2ndf1  6286  cnvoprab  6292  brtpos2  6309  tpossym  6334  frecsuclem  6464  nntri3or  6551  erth2  6639  brecop  6684  erovlem  6686  ecopovsym  6690  ecopovsymg  6693  xpcomco  6885  mapen  6907  nneneq  6918  supelti  7068  djuf1olem  7119  eldju  7134  omp1eomlem  7160  nninfwlporlemd  7238  exmidontriimlem3  7290  ordpipqqs  7441  addcanprg  7683  ltsrprg  7814  caucvgsrlemcl  7856  caucvgsrlemfv  7858  elreal  7895  ltresr  7906  axcaucvglemcl  7962  axcaucvglemval  7964  addsubeq4  8241  subcan2  8251  negcon1  8278  negcon2  8279  addid0  8399  divmulap2  8703  conjmulap  8756  rerecclap  8757  creur  8986  creui  8987  nndiv  9031  elznn0  9341  zltnle  9372  uzm1  9632  divfnzn  9695  zq  9700  icoshftf1o  10066  iccf1o  10079  fzen  10118  fzneuz  10176  4fvwrd4  10215  qltnle  10333  flqeqceilz  10410  modq0  10421  modqmuladdnn0  10460  addmodlteq  10490  nn0ennn  10525  uzennn  10528  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  seq3f1olemstep  10606  exp3val  10633  qsqeqor  10742  hashfacen  10928  cjreb  11031  caucvgrelemrec  11144  minmax  11395  xrnegiso  11427  xrnegcon1d  11429  xrminmax  11430  pwm1geoserap1  11673  dvdsval2  11955  dvdsabseq  12012  dvdsflip  12016  odd2np1  12038  oddm1even  12040  sqoddm1div8z  12051  m1exp1  12066  divalgb  12090  modremain  12094  zeqzmulgcd  12137  dfgcd2  12181  divgcdcoprm0  12269  prm2orodd  12294  hashdvds  12389  oddprmdvds  12523  oddennn  12609  evenennn  12610  gsumval2  13040  grpid  13171  grpinvcnv  13200  grplmulf1o  13206  grpsubeq0  13218  grpsubadd  13220  grplactcnv  13234  isnsg4  13342  eqg0el  13359  conjghm  13406  conjnmzb  13410  dvdsr02  13661  01eq0ring  13745  rmodislmodlem  13906  rspsn  14090  zndvds  14205  znleval  14209  toponsspwpwg  14258  dmtopon  14259  hmeoimaf1o  14550  txhmeo  14555  limcmpted  14899  ioocosf1o  15090  fsumdvdsmul  15227  gausslemma2dlem0i  15298  lgseisenlem2  15312  lgsquadlem2  15319  2lgslem1c  15331  2lgsoddprmlem2  15347  2lgsoddprm  15354  bj-peano4  15601  pwle2  15643  subctctexmid  15645  pw1nct  15647  exmidsbthrlem  15666  iooref1o  15678  iswomni0  15695