Theorem risset 3211

Description: Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
risset	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem risset

Step	Hyp	Ref	Expression
1		exancom 1862	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3061	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2812	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 304	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-rex 3061

This theorem is referenced by:  nelb  3212  ceqsralv  3481  clel5  3619  reueq  3695  reuind  3711  0el  4315  reusv3  5350  elidinxp  6003  sucel  6393  fvmptt  6961  releldm2  7987  qsid  8718  ttrcltr  9625  zorng  10414  rereccl  11859  nndiv  12191  incexc2  15761  ruclem12  16166  chnfi  18557  conjnmzb  19182  pgpfac1lem2  20006  pgpfac1lem4  20009  mat1dimelbas  22415  mat1dimbas  22416  chmaidscmat  22792  unisngl  23471  fmid  23904  dcubic  26812  addsrid  27960  addsprop  27972  negsprop  28031  mulsrid  28109  mulsprop  28126  onsfi  28352  fusgrn0degnn0  29573  chscllem2  31713  disjunsn  32669  grplsm0l  33484  ballotlemsima  34673  dfon2lem8  35982  brimg  36129  dfrecs2  36144  altopelaltxp  36170  prtlem9  39124  prter2  39141  2llnmat  39784  2lnat  40044  cdlemefrs29bpre1  40657  elnn0rabdioph  43045  fiphp3d  43061  minregex  43775