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  3779  preqr1g  3891  preqr1  3893  invdisj  4123  opthg2  4379  copsex4g  4387  opcom  4391  opeqsn  4393  opeqpr  4394  reusv3  4606  suc11g  4704  opthprc  4826  elxp3  4829  relop  4930  dmopab3  4994  rncoeq  5056  restidsing  5119  dfrel4v  5239  dmsnm  5253  iota1  5352  sniota  5368  dffn5im  5748  fvelrnb  5750  dfimafn2  5752  funimass4  5753  fnsnfv  5762  dmfco  5773  fndmdif  5814  fneqeql  5817  rexrn  5845  ralrn  5846  elrnrexdmb  5848  dffo4  5856  ftpg  5899  fconstfvm  5933  dfimafnf  5955  foima2  5957  rexima  5960  ralima  5961  dff13  5974  f1eqcocnv  5997  riotaeqimp  6063  eusvobj2  6071  f1ocnvfv3  6074  oprabid  6117  eloprabga  6175  ovelimab  6240  dfoprab3  6425  f1o2ndf1  6464  cnvoprab  6470  brtpos2  6522  tpossym  6547  frecsuclem  6677  nntri3or  6766  erth2  6854  brecop  6899  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  xpcomco  7124  mapen  7146  nneneq  7158  supelti  7342  djuf1olem  7393  eldju  7408  omp1eomlem  7434  nninfwlporlemd  7512  exmidontriimlem3  7579  ordpipqqs  7741  addcanprg  7983  ltsrprg  8114  caucvgsrlemcl  8156  caucvgsrlemfv  8158  elreal  8195  ltresr  8206  axcaucvglemcl  8262  axcaucvglemval  8264  addsubeq4  8541  subcan2  8551  negcon1  8578  negcon2  8579  addid0  8699  addeq0  8703  divmulap2  9006  conjmulap  9059  rerecclap  9060  creur  9289  creui  9290  nndiv  9345  elznn0  9659  zltnle  9690  uzm1  9953  divfnzn  10021  zq  10026  icoshftf1o  10393  iccf1o  10407  fzen  10447  fzneuz  10508  4fvwrd4  10547  qltnle  10678  flqeqceilz  10755  modq0  10766  modqmuladdnn0  10805  addmodlteq  10835  nn0ennn  10870  uzennn  10873  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  seq3f1olemstep  10951  exp3val  10978  qsqeqor  11087  hashfacen  11284  hashf1lem1  11285  wrd2ind  11495  cjreb  11631  caucvgrelemrec  11745  minmax  11996  xrnegiso  12028  xrnegcon1d  12030  xrminmax  12031  pwm1geoserap1  12275  dvdsval2  12557  dvdsabseq  12614  dvdsflip  12618  odd2np1  12640  oddm1even  12642  sqoddm1div8z  12653  m1exp1  12668  divalgb  12692  modremain  12696  zeqzmulgcd  12747  dfgcd2  12791  divgcdcoprm0  12879  prm2orodd  12904  hashdvds  12999  oddprmdvds  13133  ballotfilemsima  13259  oddennn  13283  evenennn  13284  gzsumval2  13714  grpid  13844  grpinvcnv  13873  grplmulf1o  13879  grpsubeq0  13891  grpsubadd  13893  grplactcnv  13907  isnsg4  14015  eqg0el  14032  conjghm  14079  conjnmzb  14083  dvdsr02  14412  01eq0ring  14496  rmodislmodlem  14687  rspsn  14871  zndvds  14984  znleval  14988  psrbagconf1o  15064  psr1clfi  15079  toponsspwpwg  15123  dmtopon  15124  hmeoimaf1o  15415  txhmeo  15420  limcmpted  15764  ioocosf1o  15955  fsumdvdsmul  16105  gausslemma2dlem0i  16176  lgseisenlem2  16190  lgsquadlem2  16197  2lgslem1c  16209  2lgsoddprmlem2  16225  2lgsoddprm  16232  uspgredgiedg  16419  uspgriedgedg  16420  uspgr2wlkeq  16606  wlk0prc  16613  wlklenvclwlk  16614  eupth2lem2dc  16700  bj-peano4  16981  pwle2  17028  subctctexmid  17030  pw1nct  17033  rabid1o  17034  stnot  17039  exmidsbthrlem  17067  iooref1o  17083  iswomni0  17101