Theorem risset 3238

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-rex 3088

This theorem is used by:  nelb  3239  ceqsralv  3491  clel5  3619  reueq  3695  reuind  3711  0el  4311  reusv3  5367  elidinxp  6036  sucel  6438  fvmptt  7012  releldm2  8052  qsid  8795  ttrcltr  9710  zorng  10575  rereccl  12028  nndiv  12377  incexc2  16000  ruclem12  16402  chnfi  18801  conjnmzb  19460  pgpfac1lem2  20284  pgpfac1lem4  20287  mat1dimelbas  22779  mat1dimbas  22780  chmaidscmat  23159  unisngl  23839  fmid  24272  dcubic  27167  addsrid  28343  addsprop  28355  negsprop  28414  mulsrid  28492  mulsprop  28509  onsfi  28735  fusgrn0degnn0  30073  chscllem2  32233  disjunsn  33181  grplsm0l  33947  ballotlemsima  35141  dfon2lem8  36532  brimg  36679  dfrecs2  36694  altopelaltxp  36721  prtlem9  39901  prter2  39918  2llnmat  40561  2lnat  40821  cdlemefrs29bpre1  41434  elnn0rabdioph  43789  fiphp3d  43805  minregex  44519