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  5837  fconstfvm  5871  foima2  5891  rexima  5894  ralima  5895  dff13  5908  f1eqcocnv  5931  riotaeqimp  5995  eusvobj2  6003  f1ocnvfv3  6006  oprabid  6049  eloprabga  6107  ovelimab  6172  dfoprab3  6353  f1o2ndf1  6392  cnvoprab  6398  brtpos2  6416  tpossym  6441  frecsuclem  6571  nntri3or  6660  erth2  6748  brecop  6793  erovlem  6795  ecopovsym  6799  ecopovsymg  6802  xpcomco  7009  mapen  7031  nneneq  7042  supelti  7200  djuf1olem  7251  eldju  7266  omp1eomlem  7292  nninfwlporlemd  7370  exmidontriimlem3  7437  ordpipqqs  7593  addcanprg  7835  ltsrprg  7966  caucvgsrlemcl  8008  caucvgsrlemfv  8010  elreal  8047  ltresr  8058  axcaucvglemcl  8114  axcaucvglemval  8116  addsubeq4  8393  subcan2  8403  negcon1  8430  negcon2  8431  addid0  8551  divmulap2  8855  conjmulap  8908  rerecclap  8909  creur  9138  creui  9139  nndiv  9183  elznn0  9493  zltnle  9524  uzm1  9786  divfnzn  9854  zq  9859  icoshftf1o  10225  iccf1o  10238  fzen  10277  fzneuz  10335  4fvwrd4  10374  qltnle  10502  flqeqceilz  10579  modq0  10590  modqmuladdnn0  10629  addmodlteq  10659  nn0ennn  10694  uzennn  10697  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  seq3f1olemstep  10775  exp3val  10802  qsqeqor  10911  hashfacen  11099  wrd2ind  11303  cjreb  11426  caucvgrelemrec  11539  minmax  11790  xrnegiso  11822  xrnegcon1d  11824  xrminmax  11825  pwm1geoserap1  12068  dvdsval2  12350  dvdsabseq  12407  dvdsflip  12411  odd2np1  12433  oddm1even  12435  sqoddm1div8z  12446  m1exp1  12461  divalgb  12485  modremain  12489  zeqzmulgcd  12540  dfgcd2  12584  divgcdcoprm0  12672  prm2orodd  12697  hashdvds  12792  oddprmdvds  12926  oddennn  13012  evenennn  13013  gsumval2  13479  grpid  13621  grpinvcnv  13650  grplmulf1o  13656  grpsubeq0  13668  grpsubadd  13670  grplactcnv  13684  isnsg4  13798  eqg0el  13815  conjghm  13862  conjnmzb  13866  dvdsr02  14118  01eq0ring  14202  rmodislmodlem  14363  rspsn  14547  zndvds  14662  znleval  14666  psr1clfi  14701  toponsspwpwg  14745  dmtopon  14746  hmeoimaf1o  15037  txhmeo  15042  limcmpted  15386  ioocosf1o  15577  fsumdvdsmul  15714  gausslemma2dlem0i  15785  lgseisenlem2  15799  lgsquadlem2  15806  2lgslem1c  15818  2lgsoddprmlem2  15834  2lgsoddprm  15841  uspgredgiedg  16028  uspgriedgedg  16029  uspgr2wlkeq  16215  wlk0prc  16222  wlklenvclwlk  16223  eupth2lem2dc  16309  bj-peano4  16550  pwle2  16599  subctctexmid  16601  pw1nct  16604  exmidsbthrlem  16626  iooref1o  16638  iswomni0  16655