Theorem eqcom 2142

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 1447	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2134	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2134	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 211	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 104  ∀wal 1330   = wceq 1332   ∈ wcel 1481

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 1424  ax-gen 1426  ax-ext 2122

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

This theorem is referenced by:  eqcoms  2143  eqcomi  2144  neqcomd  2145  eqcomd  2146  eqeq2  2150  eqtr2  2159  eqtr3  2160  abeq1  2250  nesym  2354  pm13.181  2391  necom  2393  gencbvex  2735  gencbval  2737  eqsbc3r  2973  dfss  3090  dfss5  3286  rabrsndc  3599  preqr1g  3701  preqr1  3703  invdisj  3931  opthg2  4169  copsex4g  4177  opcom  4180  opeqsn  4182  opeqpr  4183  reusv3  4389  suc11g  4480  opthprc  4598  elxp3  4601  relop  4697  dmopab3  4760  rncoeq  4820  dfrel4v  4998  dmsnm  5012  iota1  5110  sniota  5123  dffn5im  5475  fvelrnb  5477  dfimafn2  5479  funimass4  5480  fnsnfv  5488  dmfco  5497  fndmdif  5533  fneqeql  5536  rexrn  5565  ralrn  5566  elrnrexdmb  5568  dffo4  5576  ftpg  5612  fconstfvm  5646  foima2  5661  rexima  5664  ralima  5665  dff13  5677  f1eqcocnv  5700  eusvobj2  5768  f1ocnvfv3  5771  oprabid  5811  eloprabga  5866  ovelimab  5929  dfoprab3  6097  f1o2ndf1  6133  cnvoprab  6139  brtpos2  6156  tpossym  6181  frecsuclem  6311  nntri3or  6397  erth2  6482  brecop  6527  erovlem  6529  ecopovsym  6533  ecopovsymg  6536  xpcomco  6728  mapen  6748  nneneq  6759  supelti  6897  djuf1olem  6946  eldju  6961  omp1eomlem  6987  ordpipqqs  7206  addcanprg  7448  ltsrprg  7579  caucvgsrlemcl  7621  caucvgsrlemfv  7623  elreal  7660  ltresr  7671  axcaucvglemcl  7727  axcaucvglemval  7729  addsubeq4  8001  subcan2  8011  negcon1  8038  negcon2  8039  addid0  8159  divmulap2  8460  conjmulap  8513  rerecclap  8514  creur  8741  creui  8742  nndiv  8785  elznn0  9093  zltnle  9124  uzm1  9380  divfnzn  9440  zq  9445  icoshftf1o  9804  iccf1o  9817  fzen  9854  fzneuz  9912  4fvwrd4  9948  qltnle  10054  flqeqceilz  10122  modq0  10133  modqmuladdnn0  10172  addmodlteq  10202  nn0ennn  10237  uzennn  10240  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  seq3f1olemstep  10305  exp3val  10326  hashfacen  10611  cjreb  10670  caucvgrelemrec  10783  minmax  11033  xrnegiso  11063  xrnegcon1d  11065  xrminmax  11066  pwm1geoserap1  11309  dvdsval2  11532  dvdsabseq  11581  dvdsflip  11585  odd2np1  11606  oddm1even  11608  sqoddm1div8z  11619  m1exp1  11634  divalgb  11658  modremain  11662  zeqzmulgcd  11695  dfgcd2  11738  divgcdcoprm0  11818  prm2orodd  11843  hashdvds  11933  oddennn  11941  evenennn  11942  toponsspwpwg  12228  dmtopon  12229  hmeoimaf1o  12522  txhmeo  12527  limcmpted  12840  ioocosf1o  12983  bj-peano4  13324  pwle2  13366  subctctexmid  13369  pw1nct  13371  exmidsbthrlem  13392  iooref1o  13426