Theorem eqcom 2234

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 140	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
2	1	albii 1519	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2226	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2226	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225

This theorem is referenced by:  eqcoms  2235  eqcomi  2236  neqcomd  2237  eqcomd  2238  eqeq2  2242  eqtr2  2251  eqtr3  2252  abeq1  2342  eqabcb  2369  nesym  2457  pm13.181  2494  necom  2496  gencbvex  2861  gencbval  2863  clel5  2954  eqsbc2  3103  dfss  3225  dfss5  3426  rabrsndc  3759  preqr1g  3870  preqr1  3872  invdisj  4102  opthg2  4355  copsex4g  4363  opcom  4367  opeqsn  4369  opeqpr  4370  reusv3  4581  suc11g  4679  opthprc  4801  elxp3  4804  relop  4905  dmopab3  4969  rncoeq  5031  restidsing  5094  dfrel4v  5214  dmsnm  5228  iota1  5327  sniota  5343  dffn5im  5722  fvelrnb  5724  dfimafn2  5726  funimass4  5727  fnsnfv  5736  dmfco  5745  fndmdif  5783  fneqeql  5786  rexrn  5814  ralrn  5815  elrnrexdmb  5817  dffo4  5825  ftpg  5868  fconstfvm  5902  foima2  5924  rexima  5927  ralima  5928  dff13  5941  f1eqcocnv  5964  riotaeqimp  6028  eusvobj2  6036  f1ocnvfv3  6039  oprabid  6082  eloprabga  6140  ovelimab  6205  dfoprab3  6385  f1o2ndf1  6424  cnvoprab  6430  brtpos2  6482  tpossym  6507  frecsuclem  6637  nntri3or  6726  erth2  6814  brecop  6859  erovlem  6861  ecopovsym  6865  ecopovsymg  6868  xpcomco  7077  mapen  7099  nneneq  7111  supelti  7293  djuf1olem  7344  eldju  7359  omp1eomlem  7385  nninfwlporlemd  7463  exmidontriimlem3  7530  ordpipqqs  7689  addcanprg  7931  ltsrprg  8062  caucvgsrlemcl  8104  caucvgsrlemfv  8106  elreal  8143  ltresr  8154  axcaucvglemcl  8210  axcaucvglemval  8212  addsubeq4  8488  subcan2  8498  negcon1  8525  negcon2  8526  addid0  8646  divmulap2  8950  conjmulap  9003  rerecclap  9004  creur  9233  creui  9234  nndiv  9278  elznn0  9592  zltnle  9623  uzm1  9885  divfnzn  9953  zq  9958  icoshftf1o  10324  iccf1o  10338  fzen  10377  fzneuz  10435  4fvwrd4  10474  qltnle  10603  flqeqceilz  10680  modq0  10691  modqmuladdnn0  10730  addmodlteq  10760  nn0ennn  10795  uzennn  10798  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  seq3f1olemstep  10876  exp3val  10903  qsqeqor  11012  hashfacen  11208  wrd2ind  11415  cjreb  11551  caucvgrelemrec  11664  minmax  11915  xrnegiso  11947  xrnegcon1d  11949  xrminmax  11950  pwm1geoserap1  12194  dvdsval2  12476  dvdsabseq  12533  dvdsflip  12537  odd2np1  12559  oddm1even  12561  sqoddm1div8z  12572  m1exp1  12587  divalgb  12611  modremain  12615  zeqzmulgcd  12666  dfgcd2  12710  divgcdcoprm0  12798  prm2orodd  12823  hashdvds  12918  oddprmdvds  13052  oddennn  13143  evenennn  13144  gsumval2  13610  grpid  13752  grpinvcnv  13781  grplmulf1o  13787  grpsubeq0  13799  grpsubadd  13801  grplactcnv  13815  isnsg4  13929  eqg0el  13946  conjghm  13993  conjnmzb  13997  dvdsr02  14250  01eq0ring  14334  rmodislmodlem  14498  rspsn  14682  zndvds  14797  znleval  14801  psrbagconf1o  14828  psr1clfi  14843  toponsspwpwg  14887  dmtopon  14888  hmeoimaf1o  15179  txhmeo  15184  limcmpted  15528  ioocosf1o  15719  fsumdvdsmul  15859  gausslemma2dlem0i  15930  lgseisenlem2  15944  lgsquadlem2  15951  2lgslem1c  15963  2lgsoddprmlem2  15979  2lgsoddprm  15986  uspgredgiedg  16173  uspgriedgedg  16174  uspgr2wlkeq  16360  wlk0prc  16367  wlklenvclwlk  16368  eupth2lem2dc  16454  bj-peano4  16725  pwle2  16772  subctctexmid  16774  pw1nct  16777  exmidsbthrlem  16802  iooref1o  16818  iswomni0  16836