Theorem eqcom 2240

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

This proof depends on syntax axioms:   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqcoms  2241  eqcomi  2242  neqcomd  2243  eqcomd  2244  eqeq2  2248  eqtr2  2257  eqtr3  2258  abeq1  2348  eqabcbw  2376  eqabcb  2377  nesym  2465  pm13.181  2502  necom  2504  gencbvex  2869  gencbval  2871  clel5  2963  eqsbc2  3112  dfss  3234  dfss5  3436  rabrsndc  3778  preqr1g  3889  preqr1  3891  invdisj  4121  opthg2  4377  copsex4g  4385  opcom  4389  opeqsn  4391  opeqpr  4392  reusv3  4604  suc11g  4702  opthprc  4824  elxp3  4827  relop  4928  dmopab3  4992  rncoeq  5054  restidsing  5117  dfrel4v  5237  dmsnm  5251  iota1  5350  sniota  5366  dffn5im  5745  fvelrnb  5747  dfimafn2  5749  funimass4  5750  fnsnfv  5759  dmfco  5770  fndmdif  5808  fneqeql  5811  rexrn  5839  ralrn  5840  elrnrexdmb  5842  dffo4  5850  ftpg  5893  fconstfvm  5927  dfimafnf  5949  foima2  5951  rexima  5954  ralima  5955  dff13  5968  f1eqcocnv  5991  riotaeqimp  6057  eusvobj2  6065  f1ocnvfv3  6068  oprabid  6111  eloprabga  6169  ovelimab  6234  dfoprab3  6419  f1o2ndf1  6458  cnvoprab  6464  brtpos2  6516  tpossym  6541  frecsuclem  6671  nntri3or  6760  erth2  6848  brecop  6893  erovlem  6895  ecopovsym  6899  ecopovsymg  6902  xpcomco  7118  mapen  7140  nneneq  7152  supelti  7336  djuf1olem  7387  eldju  7402  omp1eomlem  7428  nninfwlporlemd  7506  exmidontriimlem3  7573  ordpipqqs  7735  addcanprg  7977  ltsrprg  8108  caucvgsrlemcl  8150  caucvgsrlemfv  8152  elreal  8189  ltresr  8200  axcaucvglemcl  8256  axcaucvglemval  8258  addsubeq4  8535  subcan2  8545  negcon1  8572  negcon2  8573  addid0  8693  addeq0  8697  divmulap2  9000  conjmulap  9053  rerecclap  9054  creur  9283  creui  9284  nndiv  9328  elznn0  9642  zltnle  9673  uzm1  9936  divfnzn  10004  zq  10009  icoshftf1o  10376  iccf1o  10390  fzen  10430  fzneuz  10491  4fvwrd4  10530  qltnle  10661  flqeqceilz  10738  modq0  10749  modqmuladdnn0  10788  addmodlteq  10818  nn0ennn  10853  uzennn  10856  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemab  10922  seq3f1olemstep  10934  exp3val  10961  qsqeqor  11070  hashfacen  11267  hashf1lem1  11268  wrd2ind  11478  cjreb  11614  caucvgrelemrec  11728  minmax  11979  xrnegiso  12011  xrnegcon1d  12013  xrminmax  12014  pwm1geoserap1  12258  dvdsval2  12540  dvdsabseq  12597  dvdsflip  12601  odd2np1  12623  oddm1even  12625  sqoddm1div8z  12636  m1exp1  12651  divalgb  12675  modremain  12679  zeqzmulgcd  12730  dfgcd2  12774  divgcdcoprm0  12862  prm2orodd  12887  hashdvds  12982  oddprmdvds  13116  ballotfilemsima  13242  oddennn  13266  evenennn  13267  gzsumval2  13697  grpid  13827  grpinvcnv  13856  grplmulf1o  13862  grpsubeq0  13874  grpsubadd  13876  grplactcnv  13890  isnsg4  13998  eqg0el  14015  conjghm  14062  conjnmzb  14066  dvdsr02  14395  01eq0ring  14479  rmodislmodlem  14670  rspsn  14854  zndvds  14967  znleval  14971  psrbagconf1o  15047  psr1clfi  15062  toponsspwpwg  15106  dmtopon  15107  hmeoimaf1o  15398  txhmeo  15403  limcmpted  15747  ioocosf1o  15938  fsumdvdsmul  16088  gausslemma2dlem0i  16159  lgseisenlem2  16173  lgsquadlem2  16180  2lgslem1c  16192  2lgsoddprmlem2  16208  2lgsoddprm  16215  uspgredgiedg  16402  uspgriedgedg  16403  uspgr2wlkeq  16589  wlk0prc  16596  wlklenvclwlk  16597  eupth2lem2dc  16683  bj-peano4  16964  pwle2  17011  subctctexmid  17013  pw1nct  17016  stnot  17021  exmidsbthrlem  17042  iooref1o  17058  iswomni0  17076