Theorem eqcom 2139

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 139	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1446	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2131	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2131	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 211	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 104   A.wal 1329   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  eqcoms  2140  eqcomi  2141  neqcomd  2142  eqcomd  2143  eqeq2  2147  eqtr2  2156  eqtr3  2157  abeq1  2247  nesym  2351  pm13.181  2388  necom  2390  gencbvex  2727  gencbval  2729  eqsbc3r  2964  dfss  3080  dfss5  3276  rabrsndc  3586  preqr1g  3688  preqr1  3690  invdisj  3918  opthg2  4156  copsex4g  4164  opcom  4167  opeqsn  4169  opeqpr  4170  reusv3  4376  suc11g  4467  opthprc  4585  elxp3  4588  relop  4684  dmopab3  4747  rncoeq  4807  dfrel4v  4985  dmsnm  4999  iota1  5097  sniota  5110  dffn5im  5460  fvelrnb  5462  dfimafn2  5464  funimass4  5465  fnsnfv  5473  dmfco  5482  fndmdif  5518  fneqeql  5521  rexrn  5550  ralrn  5551  elrnrexdmb  5553  dffo4  5561  ftpg  5597  fconstfvm  5631  foima2  5646  rexima  5649  ralima  5650  dff13  5662  f1eqcocnv  5685  eusvobj2  5753  f1ocnvfv3  5756  oprabid  5796  eloprabga  5851  ovelimab  5914  dfoprab3  6082  f1o2ndf1  6118  cnvoprab  6124  brtpos2  6141  tpossym  6166  frecsuclem  6296  nntri3or  6382  erth2  6467  brecop  6512  erovlem  6514  ecopovsym  6518  ecopovsymg  6521  xpcomco  6713  mapen  6733  nneneq  6744  supelti  6882  djuf1olem  6931  eldju  6946  omp1eomlem  6972  ordpipqqs  7175  addcanprg  7417  ltsrprg  7548  caucvgsrlemcl  7590  caucvgsrlemfv  7592  elreal  7629  ltresr  7640  axcaucvglemcl  7696  axcaucvglemval  7698  addsubeq4  7970  subcan2  7980  negcon1  8007  negcon2  8008  addid0  8128  divmulap2  8429  conjmulap  8482  rerecclap  8483  creur  8710  creui  8711  nndiv  8754  elznn0  9062  zltnle  9093  uzm1  9349  divfnzn  9406  zq  9411  icoshftf1o  9767  iccf1o  9780  fzen  9816  fzneuz  9874  4fvwrd4  9910  qltnle  10016  flqeqceilz  10084  modq0  10095  modqmuladdnn0  10134  addmodlteq  10164  nn0ennn  10199  uzennn  10202  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  seq3f1olemstep  10267  exp3val  10288  hashfacen  10572  cjreb  10631  caucvgrelemrec  10744  minmax  10994  xrnegiso  11024  xrnegcon1d  11026  xrminmax  11027  pwm1geoserap1  11270  dvdsval2  11485  dvdsabseq  11534  dvdsflip  11538  odd2np1  11559  oddm1even  11561  sqoddm1div8z  11572  m1exp1  11587  divalgb  11611  modremain  11615  zeqzmulgcd  11648  dfgcd2  11691  divgcdcoprm0  11771  prm2orodd  11796  hashdvds  11886  oddennn  11894  evenennn  11895  toponsspwpwg  12178  dmtopon  12179  hmeoimaf1o  12472  txhmeo  12477  limcmpted  12790  bj-peano4  13142  pwle2  13182  subctctexmid  13185  exmidsbthrlem  13206