Theorem risset 3246

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-rex 3096

This theorem is referenced by:  nelb  3247  ceqsralv  3503  clel5  3633  reueq  3709  reuind  3725  0el  4325  reusv3  5374  elidinxp  6044  sucel  6434  fvmptt  7008  releldm2  8036  qsid  8775  ttrcltr  9681  zorng  10484  rereccl  11929  nndiv  12278  incexc2  15888  ruclem12  16293  chnfi  18686  conjnmzb  19319  pgpfac1lem2  20143  pgpfac1lem4  20146  mat1dimelbas  22593  mat1dimbas  22594  chmaidscmat  22970  unisngl  23649  fmid  24082  dcubic  26973  addsrid  28119  addsprop  28131  negsprop  28190  mulsrid  28268  mulsprop  28285  onsfi  28511  fusgrn0degnn0  29786  chscllem2  31927  disjunsn  32876  grplsm0l  33652  ballotlemsima  34847  dfon2lem8  36175  brimg  36322  dfrecs2  36337  altopelaltxp  36363  prtlem9  39523  prter2  39540  2llnmat  40183  2lnat  40443  cdlemefrs29bpre1  41056  elnn0rabdioph  43415  fiphp3d  43431  minregex  44145