Theorem risset 3226

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 3112	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2871	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 307	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2870  df-rex 3112

This theorem is referenced by:  nelb  3227  clel5  3605  reueq  3676  reuind  3692  0el  4274  iunid  4947  reusv3  5271  elidinxp  5878  sucel  6232  fvmptt  6765  releldm2  7724  qsid  8346  zorng  9915  rereccl  11347  nndiv  11671  incexc2  15185  ruclem12  15586  conjnmzb  18385  pgpfac1lem2  19190  pgpfac1lem4  19193  mat1dimelbas  21076  mat1dimbas  21077  chmaidscmat  21453  unisngl  22132  fmid  22565  dcubic  25432  fusgrn0degnn0  27289  chscllem2  29421  disjunsn  30357  ballotlemsima  31883  dfon2lem8  33148  brimg  33511  dfrecs2  33524  altopelaltxp  33550  prtlem9  36160  prter2  36177  2llnmat  36820  2lnat  37080  cdlemefrs29bpre1  37693  elnn0rabdioph  39744  fiphp3d  39760