Theorem eqcom 2102

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqcom	⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Proof of Theorem eqcom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 139	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
2	1	albii 1414	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2094	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2094	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 211	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 104  ∀wal 1297   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ext 2082

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

This theorem is referenced by:  eqcoms  2103  eqcomi  2104  eqcomd  2105  eqeq2  2109  eqtr2  2118  eqtr3  2119  abeq1  2209  nesym  2312  pm13.181  2349  necom  2351  gencbvex  2687  gencbval  2689  eqsbc3r  2921  dfss  3035  dfss5  3228  rabrsndc  3538  preqr1g  3640  preqr1  3642  invdisj  3869  opthg2  4099  copsex4g  4107  opcom  4110  opeqsn  4112  opeqpr  4113  reusv3  4319  suc11g  4410  opthprc  4528  elxp3  4531  relop  4627  dmopab3  4690  rncoeq  4748  dfrel4v  4926  dmsnm  4940  iota1  5038  sniota  5051  dffn5im  5399  fvelrnb  5401  dfimafn2  5403  funimass4  5404  fnsnfv  5412  dmfco  5421  fndmdif  5457  fneqeql  5460  rexrn  5489  ralrn  5490  elrnrexdmb  5492  dffo4  5500  ftpg  5536  fconstfvm  5570  foima2  5585  rexima  5588  ralima  5589  dff13  5601  f1eqcocnv  5624  eusvobj2  5692  f1ocnvfv3  5695  oprabid  5735  eloprabga  5790  ovelimab  5853  dfoprab3  6019  f1o2ndf1  6055  cnvoprab  6061  brtpos2  6078  tpossym  6103  frecsuclem  6233  nntri3or  6319  erth2  6404  brecop  6449  erovlem  6451  ecopovsym  6455  ecopovsymg  6458  xpcomco  6649  mapen  6669  nneneq  6680  supelti  6804  djuf1olem  6853  eldju  6868  omp1eomlem  6894  ordpipqqs  7083  addcanprg  7325  ltsrprg  7443  caucvgsrlemcl  7484  caucvgsrlemfv  7486  elreal  7516  ltresr  7526  axcaucvglemcl  7580  axcaucvglemval  7582  addsubeq4  7848  subcan2  7858  negcon1  7885  negcon2  7886  addid0  8002  divmulap2  8297  conjmulap  8350  rerecclap  8351  creur  8575  creui  8576  nndiv  8619  elznn0  8921  zltnle  8952  uzm1  9206  divfnzn  9263  zq  9268  icoshftf1o  9615  iccf1o  9628  fzen  9664  fzneuz  9722  4fvwrd4  9758  qltnle  9864  flqeqceilz  9932  modq0  9943  modqmuladdnn0  9982  addmodlteq  10012  nn0ennn  10047  uzennn  10050  iseqf1olemqcl  10100  iseqf1olemnab  10102  iseqf1olemab  10103  seq3f1olemstep  10115  exp3val  10136  hashfacen  10420  cjreb  10479  caucvgrelemrec  10591  minmax  10840  xrnegiso  10870  xrnegcon1d  10872  xrminmax  10873  pwm1geoserap1  11116  dvdsval2  11291  dvdsabseq  11340  dvdsflip  11344  odd2np1  11365  oddm1even  11367  sqoddm1div8z  11378  m1exp1  11393  divalgb  11417  modremain  11421  zeqzmulgcd  11454  dfgcd2  11495  divgcdcoprm0  11575  prm2orodd  11600  hashdvds  11689  oddennn  11697  evenennn  11698  toponsspwpwg  11971  dmtopon  11972  bj-peano4  12738  pwle2  12779  exmidsbthrlem  12801