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

Syntax hints:   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ 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 1496  ax-gen 1498  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  2448  pm13.181  2485  necom  2487  gencbvex  2851  gencbval  2853  clel5  2944  eqsbc2  3093  dfss  3215  dfss5  3414  rabrsndc  3743  preqr1g  3854  preqr1  3856  invdisj  4086  opthg2  4337  copsex4g  4345  opcom  4349  opeqsn  4351  opeqpr  4352  reusv3  4563  suc11g  4661  opthprc  4783  elxp3  4786  relop  4886  dmopab3  4950  rncoeq  5012  restidsing  5075  dfrel4v  5195  dmsnm  5209  iota1  5308  sniota  5324  dffn5im  5700  fvelrnb  5702  dfimafn2  5704  funimass4  5705  fnsnfv  5714  dmfco  5723  fndmdif  5761  fneqeql  5764  rexrn  5792  ralrn  5793  elrnrexdmb  5795  dffo4  5803  ftpg  5846  fconstfvm  5880  foima2  5902  rexima  5905  ralima  5906  dff13  5919  f1eqcocnv  5942  riotaeqimp  6006  eusvobj2  6014  f1ocnvfv3  6017  oprabid  6060  eloprabga  6118  ovelimab  6183  dfoprab3  6363  f1o2ndf1  6402  cnvoprab  6408  brtpos2  6460  tpossym  6485  frecsuclem  6615  nntri3or  6704  erth2  6792  brecop  6837  erovlem  6839  ecopovsym  6843  ecopovsymg  6846  xpcomco  7053  mapen  7075  nneneq  7086  supelti  7244  djuf1olem  7295  eldju  7310  omp1eomlem  7336  nninfwlporlemd  7414  exmidontriimlem3  7481  ordpipqqs  7637  addcanprg  7879  ltsrprg  8010  caucvgsrlemcl  8052  caucvgsrlemfv  8054  elreal  8091  ltresr  8102  axcaucvglemcl  8158  axcaucvglemval  8160  addsubeq4  8436  subcan2  8446  negcon1  8473  negcon2  8474  addid0  8594  divmulap2  8898  conjmulap  8951  rerecclap  8952  creur  9181  creui  9182  nndiv  9226  elznn0  9538  zltnle  9569  uzm1  9831  divfnzn  9899  zq  9904  icoshftf1o  10270  iccf1o  10284  fzen  10323  fzneuz  10381  4fvwrd4  10420  qltnle  10549  flqeqceilz  10626  modq0  10637  modqmuladdnn0  10676  addmodlteq  10706  nn0ennn  10741  uzennn  10744  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemab  10810  seq3f1olemstep  10822  exp3val  10849  qsqeqor  10958  hashfacen  11146  wrd2ind  11353  cjreb  11489  caucvgrelemrec  11602  minmax  11853  xrnegiso  11885  xrnegcon1d  11887  xrminmax  11888  pwm1geoserap1  12132  dvdsval2  12414  dvdsabseq  12471  dvdsflip  12475  odd2np1  12497  oddm1even  12499  sqoddm1div8z  12510  m1exp1  12525  divalgb  12549  modremain  12553  zeqzmulgcd  12604  dfgcd2  12648  divgcdcoprm0  12736  prm2orodd  12761  hashdvds  12856  oddprmdvds  12990  oddennn  13076  evenennn  13077  gsumval2  13543  grpid  13685  grpinvcnv  13714  grplmulf1o  13720  grpsubeq0  13732  grpsubadd  13734  grplactcnv  13748  isnsg4  13862  eqg0el  13879  conjghm  13926  conjnmzb  13930  dvdsr02  14183  01eq0ring  14267  rmodislmodlem  14429  rspsn  14613  zndvds  14728  znleval  14732  psrbagconf1o  14757  psr1clfi  14772  toponsspwpwg  14816  dmtopon  14817  hmeoimaf1o  15108  txhmeo  15113  limcmpted  15457  ioocosf1o  15648  fsumdvdsmul  15788  gausslemma2dlem0i  15859  lgseisenlem2  15873  lgsquadlem2  15880  2lgslem1c  15892  2lgsoddprmlem2  15908  2lgsoddprm  15915  uspgredgiedg  16102  uspgriedgedg  16103  uspgr2wlkeq  16289  wlk0prc  16296  wlklenvclwlk  16297  eupth2lem2dc  16383  bj-peano4  16654  pwle2  16703  subctctexmid  16705  pw1nct  16708  exmidsbthrlem  16733  iooref1o  16749  iswomni0  16767