Theorem eqcom 2233

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

Syntax hints:   ↔ wb 105  ∀wal 1395   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  eqcoms  2234  eqcomi  2235  neqcomd  2236  eqcomd  2237  eqeq2  2241  eqtr2  2250  eqtr3  2251  abeq1  2341  nesym  2447  pm13.181  2484  necom  2486  gencbvex  2850  gencbval  2852  clel5  2943  eqsbc2  3092  dfss  3214  dfss5  3412  rabrsndc  3739  preqr1g  3849  preqr1  3851  invdisj  4081  opthg2  4331  copsex4g  4339  opcom  4343  opeqsn  4345  opeqpr  4346  reusv3  4557  suc11g  4655  opthprc  4777  elxp3  4780  relop  4880  dmopab3  4944  rncoeq  5006  restidsing  5069  dfrel4v  5188  dmsnm  5202  iota1  5301  sniota  5317  dffn5im  5691  fvelrnb  5693  dfimafn2  5695  funimass4  5696  fnsnfv  5705  dmfco  5714  fndmdif  5752  fneqeql  5755  rexrn  5784  ralrn  5785  elrnrexdmb  5787  dffo4  5795  ftpg  5838  fconstfvm  5872  foima2  5892  rexima  5895  ralima  5896  dff13  5909  f1eqcocnv  5932  riotaeqimp  5996  eusvobj2  6004  f1ocnvfv3  6007  oprabid  6050  eloprabga  6108  ovelimab  6173  dfoprab3  6354  f1o2ndf1  6393  cnvoprab  6399  brtpos2  6417  tpossym  6442  frecsuclem  6572  nntri3or  6661  erth2  6749  brecop  6794  erovlem  6796  ecopovsym  6800  ecopovsymg  6803  xpcomco  7010  mapen  7032  nneneq  7043  supelti  7201  djuf1olem  7252  eldju  7267  omp1eomlem  7293  nninfwlporlemd  7371  exmidontriimlem3  7438  ordpipqqs  7594  addcanprg  7836  ltsrprg  7967  caucvgsrlemcl  8009  caucvgsrlemfv  8011  elreal  8048  ltresr  8059  axcaucvglemcl  8115  axcaucvglemval  8117  addsubeq4  8394  subcan2  8404  negcon1  8431  negcon2  8432  addid0  8552  divmulap2  8856  conjmulap  8909  rerecclap  8910  creur  9139  creui  9140  nndiv  9184  elznn0  9494  zltnle  9525  uzm1  9787  divfnzn  9855  zq  9860  icoshftf1o  10226  iccf1o  10239  fzen  10278  fzneuz  10336  4fvwrd4  10375  qltnle  10504  flqeqceilz  10581  modq0  10592  modqmuladdnn0  10631  addmodlteq  10661  nn0ennn  10696  uzennn  10699  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  seq3f1olemstep  10777  exp3val  10804  qsqeqor  10913  hashfacen  11101  wrd2ind  11308  cjreb  11431  caucvgrelemrec  11544  minmax  11795  xrnegiso  11827  xrnegcon1d  11829  xrminmax  11830  pwm1geoserap1  12074  dvdsval2  12356  dvdsabseq  12413  dvdsflip  12417  odd2np1  12439  oddm1even  12441  sqoddm1div8z  12452  m1exp1  12467  divalgb  12491  modremain  12495  zeqzmulgcd  12546  dfgcd2  12590  divgcdcoprm0  12678  prm2orodd  12703  hashdvds  12798  oddprmdvds  12932  oddennn  13018  evenennn  13019  gsumval2  13485  grpid  13627  grpinvcnv  13656  grplmulf1o  13662  grpsubeq0  13674  grpsubadd  13676  grplactcnv  13690  isnsg4  13804  eqg0el  13821  conjghm  13868  conjnmzb  13872  dvdsr02  14125  01eq0ring  14209  rmodislmodlem  14370  rspsn  14554  zndvds  14669  znleval  14673  psr1clfi  14708  toponsspwpwg  14752  dmtopon  14753  hmeoimaf1o  15044  txhmeo  15049  limcmpted  15393  ioocosf1o  15584  fsumdvdsmul  15721  gausslemma2dlem0i  15792  lgseisenlem2  15806  lgsquadlem2  15813  2lgslem1c  15825  2lgsoddprmlem2  15841  2lgsoddprm  15848  uspgredgiedg  16035  uspgriedgedg  16036  uspgr2wlkeq  16222  wlk0prc  16229  wlklenvclwlk  16230  eupth2lem2dc  16316  bj-peano4  16576  pwle2  16625  subctctexmid  16627  pw1nct  16630  exmidsbthrlem  16652  iooref1o  16664  iswomni0  16682