Theorem eqcom 2042

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 128	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1359	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2034	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2034	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 201	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 98   A.wal 1241   = wceq 1243   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  eqcoms  2043  eqcomi  2044  eqcomd  2045  eqeq2  2049  eqtr2  2058  eqtr3  2059  abeq1  2147  nesym  2250  pm13.181  2287  necom  2289  gencbvex  2600  gencbval  2602  eqsbc3r  2819  dfss  2932  dfss5  3142  disj4im  3276  ssnelpss  3289  rabrsndc  3438  preqr1g  3537  preqr1  3539  invdisj  3759  opthg2  3976  copsex4g  3984  opcom  3987  opeqsn  3989  opeqpr  3990  reusv3  4192  suc11g  4281  dtruex  4283  opthprc  4391  elxp3  4394  relop  4486  dmopab3  4548  rncoeq  4605  dfrel4v  4772  dmsnm  4786  iota1  4881  sniota  4894  dffn5im  5219  fvelrnb  5221  dfimafn2  5223  funimass4  5224  fnsnfv  5232  dmfco  5241  fndmdif  5272  fneqeql  5275  rexrn  5304  ralrn  5305  elrnrexdmb  5307  dffo4  5315  ftpg  5347  fconstfvm  5379  rexima  5394  ralima  5395  dff13  5407  f1eqcocnv  5431  eusvobj2  5498  f1ocnvfv3  5501  oprabid  5537  eloprabga  5591  ovelimab  5651  dfoprab3  5817  f1o2ndf1  5849  brtpos2  5866  tpossym  5891  frecsuclem3  5990  nntri3or  6072  erth2  6151  brecop  6196  erovlem  6198  ecopovsym  6202  ecopovsymg  6205  xpcomco  6300  nneneq  6320  ordpipqqs  6472  addcanprg  6714  ltsrprg  6832  caucvgsrlemcl  6873  caucvgsrlemfv  6875  elreal  6905  ltresr  6915  axcaucvglemcl  6969  axcaucvglemval  6971  addsubeq4  7226  subcan2  7236  negcon1  7263  negcon2  7264  divmulap2  7655  conjmulap  7705  rerecclap  7706  creur  7911  creui  7912  nndiv  7954  elznn0  8260  zltnle  8291  uzm1  8503  divfnzn  8556  zq  8561  icoshftf1o  8859  iccf1o  8872  fzen  8907  fzneuz  8963  4fvwrd4  8997  qltnle  9101  flqeqceilz  9160  modq0  9171  nn0ennn  9209  cjreb  9466  caucvgrelemrec  9578  bj-peano4  10080