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 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced 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  3775  preqr1g  3886  preqr1  3888  invdisj  4118  opthg2  4374  copsex4g  4382  opcom  4386  opeqsn  4388  opeqpr  4389  reusv3  4601  suc11g  4699  opthprc  4821  elxp3  4824  relop  4925  dmopab3  4989  rncoeq  5051  restidsing  5114  dfrel4v  5234  dmsnm  5248  iota1  5347  sniota  5363  dffn5im  5742  fvelrnb  5744  dfimafn2  5746  funimass4  5747  fnsnfv  5756  dmfco  5767  fndmdif  5805  fneqeql  5808  rexrn  5836  ralrn  5837  elrnrexdmb  5839  dffo4  5847  ftpg  5890  fconstfvm  5924  dfimafnf  5945  foima2  5947  rexima  5950  ralima  5951  dff13  5964  f1eqcocnv  5987  riotaeqimp  6053  eusvobj2  6061  f1ocnvfv3  6064  oprabid  6107  eloprabga  6165  ovelimab  6230  dfoprab3  6415  f1o2ndf1  6454  cnvoprab  6460  brtpos2  6512  tpossym  6537  frecsuclem  6667  nntri3or  6756  erth2  6844  brecop  6889  erovlem  6891  ecopovsym  6895  ecopovsymg  6898  xpcomco  7114  mapen  7136  nneneq  7148  supelti  7332  djuf1olem  7383  eldju  7398  omp1eomlem  7424  nninfwlporlemd  7502  exmidontriimlem3  7569  ordpipqqs  7731  addcanprg  7973  ltsrprg  8104  caucvgsrlemcl  8146  caucvgsrlemfv  8148  elreal  8185  ltresr  8196  axcaucvglemcl  8252  axcaucvglemval  8254  addsubeq4  8531  subcan2  8541  negcon1  8568  negcon2  8569  addid0  8689  addeq0  8693  divmulap2  8996  conjmulap  9049  rerecclap  9050  creur  9279  creui  9280  nndiv  9324  elznn0  9638  zltnle  9669  uzm1  9932  divfnzn  10000  zq  10005  icoshftf1o  10372  iccf1o  10386  fzen  10426  fzneuz  10486  4fvwrd4  10525  qltnle  10656  flqeqceilz  10733  modq0  10744  modqmuladdnn0  10783  addmodlteq  10813  nn0ennn  10848  uzennn  10851  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  seq3f1olemstep  10929  exp3val  10956  qsqeqor  11065  hashfacen  11262  hashf1lem1  11263  wrd2ind  11473  cjreb  11609  caucvgrelemrec  11723  minmax  11974  xrnegiso  12006  xrnegcon1d  12008  xrminmax  12009  pwm1geoserap1  12253  dvdsval2  12535  dvdsabseq  12592  dvdsflip  12596  odd2np1  12618  oddm1even  12620  sqoddm1div8z  12631  m1exp1  12646  divalgb  12670  modremain  12674  zeqzmulgcd  12725  dfgcd2  12769  divgcdcoprm0  12857  prm2orodd  12882  hashdvds  12977  oddprmdvds  13111  ballotfilemsima  13237  oddennn  13261  evenennn  13262  gzsumval2  13691  grpid  13821  grpinvcnv  13850  grplmulf1o  13856  grpsubeq0  13868  grpsubadd  13870  grplactcnv  13884  isnsg4  13992  eqg0el  14009  conjghm  14056  conjnmzb  14060  dvdsr02  14385  01eq0ring  14469  rmodislmodlem  14659  rspsn  14843  zndvds  14956  znleval  14960  psrbagconf1o  14987  psr1clfi  15002  toponsspwpwg  15046  dmtopon  15047  hmeoimaf1o  15338  txhmeo  15343  limcmpted  15687  ioocosf1o  15878  fsumdvdsmul  16019  gausslemma2dlem0i  16090  lgseisenlem2  16104  lgsquadlem2  16111  2lgslem1c  16123  2lgsoddprmlem2  16139  2lgsoddprm  16146  uspgredgiedg  16333  uspgriedgedg  16334  uspgr2wlkeq  16520  wlk0prc  16527  wlklenvclwlk  16528  eupth2lem2dc  16614  bj-peano4  16895  pwle2  16942  subctctexmid  16944  pw1nct  16947  exmidsbthrlem  16972  iooref1o  16988  iswomni0  17006