Theorem risset 3194

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 1864	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2817	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 304	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816  df-rex 3070

This theorem is referenced by:  nelb  3195  nelbOLD  3196  ceqsralv  3469  clel5  3596  reueq  3672  reuind  3688  0el  4294  iunid  4990  reusv3  5328  elidinxp  5951  sucel  6339  fvmptt  6895  releldm2  7884  qsid  8572  ttrcltr  9474  zorng  10260  rereccl  11693  nndiv  12019  incexc2  15550  ruclem12  15950  conjnmzb  18869  pgpfac1lem2  19678  pgpfac1lem4  19681  mat1dimelbas  21620  mat1dimbas  21621  chmaidscmat  21997  unisngl  22678  fmid  23111  dcubic  25996  fusgrn0degnn0  27866  chscllem2  30000  disjunsn  30933  grplsm0l  31591  ballotlemsima  32482  dfon2lem8  33766  addsid1  34127  brimg  34239  dfrecs2  34252  altopelaltxp  34278  prtlem9  36878  prter2  36895  2llnmat  37538  2lnat  37798  cdlemefrs29bpre1  38411  elnn0rabdioph  40625  fiphp3d  40641  minregex  41141