Theorem eqcom 2056

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 132	. . 3 |- ( ( x e. A <-> x e. B ) <-> ( x e. B <-> x e. A ) )
2	1	albii 1373	. 2 |- ( A. x ( x e. A <-> x e. B ) <-> A. x ( x e. B <-> x e. A ) )
3		dfcleq 2048	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4		dfcleq 2048	. 2 |- ( B = A <-> A. x ( x e. B <-> x e. A ) )
5	2, 3, 4	3bitr4i 205	1 |- ( A = B <-> B = A )

Syntax hints:   <-> wb 102   A.wal 1255   = wceq 1257   e. wcel 1407

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-cleq 2047

This theorem is referenced by:  eqcoms  2057  eqcomi  2058  eqcomd  2059  eqeq2  2063  eqtr2  2072  eqtr3  2073  abeq1  2161  nesym  2263  pm13.181  2300  necom  2302  gencbvex  2615  gencbval  2617  eqsbc3r  2843  dfss  2957  dfss5  3167  disj4im  3301  ssnelpss  3314  rabrsndc  3463  preqr1g  3562  preqr1  3564  invdisj  3784  opthg2  4001  copsex4g  4009  opcom  4012  opeqsn  4014  opeqpr  4015  reusv3  4217  suc11g  4306  dtruex  4308  opthprc  4416  elxp3  4419  relop  4511  dmopab3  4573  rncoeq  4630  dfrel4v  4797  dmsnm  4811  iota1  4906  sniota  4919  dffn5im  5244  fvelrnb  5246  dfimafn2  5248  funimass4  5249  fnsnfv  5257  dmfco  5266  fndmdif  5297  fneqeql  5300  rexrn  5329  ralrn  5330  elrnrexdmb  5332  dffo4  5340  ftpg  5372  fconstfvm  5404  rexima  5419  ralima  5420  dff13  5432  f1eqcocnv  5456  eusvobj2  5523  f1ocnvfv3  5526  oprabid  5562  eloprabga  5616  ovelimab  5676  dfoprab3  5842  f1o2ndf1  5874  cnvoprab  5880  brtpos2  5894  tpossym  5919  frecsuclem3  6018  nntri3or  6100  erth2  6179  brecop  6224  erovlem  6226  ecopovsym  6230  ecopovsymg  6233  xpcomco  6328  nneneq  6348  ordpipqqs  6500  addcanprg  6742  ltsrprg  6860  caucvgsrlemcl  6901  caucvgsrlemfv  6903  elreal  6933  ltresr  6943  axcaucvglemcl  6997  axcaucvglemval  6999  addsubeq4  7259  subcan2  7269  negcon1  7296  negcon2  7297  addid0  7413  divmulap2  7699  conjmulap  7750  rerecclap  7751  creur  7957  creui  7958  nndiv  8000  elznn0  8287  zltnle  8318  uzm1  8569  divfnzn  8623  zq  8628  icoshftf1o  8930  iccf1o  8943  fzen  8979  fzneuz  9035  4fvwrd4  9069  qltnle  9173  flqeqceilz  9233  modq0  9244  modqmuladdnn0  9283  addmodlteq  9313  nn0ennn  9338  cjreb  9658  caucvgrelemrec  9770  dvdsval2  10074  dvdsabseq  10122  dvdsflip  10126  odd2np1  10147  oddm1even  10149  sqoddm1div8z  10161  m1exp1  10176  bj-peano4  10410