Theorem eqcom 2231

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

Syntax hints:   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqcoms  2232  eqcomi  2233  neqcomd  2234  eqcomd  2235  eqeq2  2239  eqtr2  2248  eqtr3  2249  abeq1  2339  nesym  2445  pm13.181  2482  necom  2484  gencbvex  2847  gencbval  2849  clel5  2940  eqsbc2  3089  dfss  3211  dfss5  3409  rabrsndc  3734  preqr1g  3843  preqr1  3845  invdisj  4075  opthg2  4324  copsex4g  4332  opcom  4336  opeqsn  4338  opeqpr  4339  reusv3  4550  suc11g  4648  opthprc  4769  elxp3  4772  relop  4871  dmopab3  4935  rncoeq  4997  restidsing  5060  dfrel4v  5179  dmsnm  5193  iota1  5292  sniota  5308  dffn5im  5678  fvelrnb  5680  dfimafn2  5682  funimass4  5683  fnsnfv  5692  dmfco  5701  fndmdif  5739  fneqeql  5742  rexrn  5771  ralrn  5772  elrnrexdmb  5774  dffo4  5782  ftpg  5822  fconstfvm  5856  foima2  5874  rexima  5877  ralima  5878  dff13  5891  f1eqcocnv  5914  riotaeqimp  5978  eusvobj2  5986  f1ocnvfv3  5989  oprabid  6032  eloprabga  6090  ovelimab  6155  dfoprab3  6335  f1o2ndf1  6372  cnvoprab  6378  brtpos2  6395  tpossym  6420  frecsuclem  6550  nntri3or  6637  erth2  6725  brecop  6770  erovlem  6772  ecopovsym  6776  ecopovsymg  6779  xpcomco  6981  mapen  7003  nneneq  7014  supelti  7165  djuf1olem  7216  eldju  7231  omp1eomlem  7257  nninfwlporlemd  7335  exmidontriimlem3  7401  ordpipqqs  7557  addcanprg  7799  ltsrprg  7930  caucvgsrlemcl  7972  caucvgsrlemfv  7974  elreal  8011  ltresr  8022  axcaucvglemcl  8078  axcaucvglemval  8080  addsubeq4  8357  subcan2  8367  negcon1  8394  negcon2  8395  addid0  8515  divmulap2  8819  conjmulap  8872  rerecclap  8873  creur  9102  creui  9103  nndiv  9147  elznn0  9457  zltnle  9488  uzm1  9749  divfnzn  9812  zq  9817  icoshftf1o  10183  iccf1o  10196  fzen  10235  fzneuz  10293  4fvwrd4  10332  qltnle  10458  flqeqceilz  10535  modq0  10546  modqmuladdnn0  10585  addmodlteq  10615  nn0ennn  10650  uzennn  10653  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  seq3f1olemstep  10731  exp3val  10758  qsqeqor  10867  hashfacen  11053  wrd2ind  11250  cjreb  11372  caucvgrelemrec  11485  minmax  11736  xrnegiso  11768  xrnegcon1d  11770  xrminmax  11771  pwm1geoserap1  12014  dvdsval2  12296  dvdsabseq  12353  dvdsflip  12357  odd2np1  12379  oddm1even  12381  sqoddm1div8z  12392  m1exp1  12407  divalgb  12431  modremain  12435  zeqzmulgcd  12486  dfgcd2  12530  divgcdcoprm0  12618  prm2orodd  12643  hashdvds  12738  oddprmdvds  12872  oddennn  12958  evenennn  12959  gsumval2  13425  grpid  13567  grpinvcnv  13596  grplmulf1o  13602  grpsubeq0  13614  grpsubadd  13616  grplactcnv  13630  isnsg4  13744  eqg0el  13761  conjghm  13808  conjnmzb  13812  dvdsr02  14063  01eq0ring  14147  rmodislmodlem  14308  rspsn  14492  zndvds  14607  znleval  14611  psr1clfi  14646  toponsspwpwg  14690  dmtopon  14691  hmeoimaf1o  14982  txhmeo  14987  limcmpted  15331  ioocosf1o  15522  fsumdvdsmul  15659  gausslemma2dlem0i  15730  lgseisenlem2  15744  lgsquadlem2  15751  2lgslem1c  15763  2lgsoddprmlem2  15779  2lgsoddprm  15786  uspgredgiedg  15970  uspgriedgedg  15971  bj-peano4  16276  pwle2  16323  subctctexmid  16325  pw1nct  16328  exmidsbthrlem  16349  iooref1o  16361  iswomni0  16378