Theorem risset 3237

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 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2836	. 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 3086

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 2835  df-rex 3087

This theorem is used by:  nelb  3238  ceqsralv  3490  clel5  3619  reueq  3695  reuind  3711  0el  4311  reusv3  5370  elidinxp  6040  sucel  6434  fvmptt  7007  releldm2  8040  qsid  8781  ttrcltr  9695  zorng  10506  rereccl  11957  nndiv  12306  incexc2  15927  ruclem12  16329  chnfi  18722  conjnmzb  19380  pgpfac1lem2  20204  pgpfac1lem4  20207  mat1dimelbas  22693  mat1dimbas  22694  chmaidscmat  23073  unisngl  23753  fmid  24186  dcubic  27083  addsrid  28229  addsprop  28241  negsprop  28300  mulsrid  28378  mulsprop  28395  onsfi  28621  fusgrn0degnn0  29959  chscllem2  32119  disjunsn  33067  grplsm0l  33832  ballotlemsima  35027  dfon2lem8  36367  brimg  36514  dfrecs2  36529  altopelaltxp  36556  prtlem9  39737  prter2  39754  2llnmat  40397  2lnat  40657  cdlemefrs29bpre1  41270  elnn0rabdioph  43644  fiphp3d  43660  minregex  44374