Theorem eqcom 2209

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 1494	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2201	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2201	. 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 2178

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 1471  ax-gen 1473  ax-ext 2189

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

This theorem is referenced by:  eqcoms  2210  eqcomi  2211  neqcomd  2212  eqcomd  2213  eqeq2  2217  eqtr2  2226  eqtr3  2227  abeq1  2317  nesym  2423  pm13.181  2460  necom  2462  gencbvex  2824  gencbval  2826  clel5  2917  eqsbc2  3066  dfss  3188  dfss5  3386  rabrsndc  3711  preqr1g  3820  preqr1  3822  invdisj  4052  opthg2  4301  copsex4g  4309  opcom  4313  opeqsn  4315  opeqpr  4316  reusv3  4525  suc11g  4623  opthprc  4744  elxp3  4747  relop  4846  dmopab3  4910  rncoeq  4971  restidsing  5034  dfrel4v  5153  dmsnm  5167  iota1  5265  sniota  5281  dffn5im  5647  fvelrnb  5649  dfimafn2  5651  funimass4  5652  fnsnfv  5661  dmfco  5670  fndmdif  5708  fneqeql  5711  rexrn  5740  ralrn  5741  elrnrexdmb  5743  dffo4  5751  ftpg  5791  fconstfvm  5825  foima2  5843  rexima  5846  ralima  5847  dff13  5860  f1eqcocnv  5883  eusvobj2  5953  f1ocnvfv3  5956  oprabid  5999  eloprabga  6055  ovelimab  6120  dfoprab3  6300  f1o2ndf1  6337  cnvoprab  6343  brtpos2  6360  tpossym  6385  frecsuclem  6515  nntri3or  6602  erth2  6690  brecop  6735  erovlem  6737  ecopovsym  6741  ecopovsymg  6744  xpcomco  6946  mapen  6968  nneneq  6979  supelti  7130  djuf1olem  7181  eldju  7196  omp1eomlem  7222  nninfwlporlemd  7300  exmidontriimlem3  7366  ordpipqqs  7522  addcanprg  7764  ltsrprg  7895  caucvgsrlemcl  7937  caucvgsrlemfv  7939  elreal  7976  ltresr  7987  axcaucvglemcl  8043  axcaucvglemval  8045  addsubeq4  8322  subcan2  8332  negcon1  8359  negcon2  8360  addid0  8480  divmulap2  8784  conjmulap  8837  rerecclap  8838  creur  9067  creui  9068  nndiv  9112  elznn0  9422  zltnle  9453  uzm1  9714  divfnzn  9777  zq  9782  icoshftf1o  10148  iccf1o  10161  fzen  10200  fzneuz  10258  4fvwrd4  10297  qltnle  10423  flqeqceilz  10500  modq0  10511  modqmuladdnn0  10550  addmodlteq  10580  nn0ennn  10615  uzennn  10618  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  seq3f1olemstep  10696  exp3val  10723  qsqeqor  10832  hashfacen  11018  wrd2ind  11214  cjreb  11292  caucvgrelemrec  11405  minmax  11656  xrnegiso  11688  xrnegcon1d  11690  xrminmax  11691  pwm1geoserap1  11934  dvdsval2  12216  dvdsabseq  12273  dvdsflip  12277  odd2np1  12299  oddm1even  12301  sqoddm1div8z  12312  m1exp1  12327  divalgb  12351  modremain  12355  zeqzmulgcd  12406  dfgcd2  12450  divgcdcoprm0  12538  prm2orodd  12563  hashdvds  12658  oddprmdvds  12792  oddennn  12878  evenennn  12879  gsumval2  13344  grpid  13486  grpinvcnv  13515  grplmulf1o  13521  grpsubeq0  13533  grpsubadd  13535  grplactcnv  13549  isnsg4  13663  eqg0el  13680  conjghm  13727  conjnmzb  13731  dvdsr02  13982  01eq0ring  14066  rmodislmodlem  14227  rspsn  14411  zndvds  14526  znleval  14530  psr1clfi  14565  toponsspwpwg  14609  dmtopon  14610  hmeoimaf1o  14901  txhmeo  14906  limcmpted  15250  ioocosf1o  15441  fsumdvdsmul  15578  gausslemma2dlem0i  15649  lgseisenlem2  15663  lgsquadlem2  15670  2lgslem1c  15682  2lgsoddprmlem2  15698  2lgsoddprm  15705  bj-peano4  16090  pwle2  16137  subctctexmid  16139  pw1nct  16142  exmidsbthrlem  16163  iooref1o  16175  iswomni0  16192