Theorem risset 3231

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

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

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 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-rex 3072

This theorem is referenced by:  nelb  3232  nelbOLD  3233  ceqsralv  3514  clel5  3656  reueq  3734  reuind  3750  0el  4361  iunidOLD  5065  reusv3  5404  elidinxp  6044  sucel  6439  fvmptt  7019  releldm2  8029  qsid  8777  ttrcltr  9711  zorng  10499  rereccl  11932  nndiv  12258  incexc2  15784  ruclem12  16184  conjnmzb  19127  pgpfac1lem2  19945  pgpfac1lem4  19948  mat1dimelbas  21973  mat1dimbas  21974  chmaidscmat  22350  unisngl  23031  fmid  23464  dcubic  26351  addsrid  27450  addsprop  27462  negsprop  27512  mulsrid  27572  mulsprop  27589  fusgrn0degnn0  28787  chscllem2  30922  disjunsn  31856  grplsm0l  32544  ballotlemsima  33545  dfon2lem8  34793  brimg  34940  dfrecs2  34953  altopelaltxp  34979  prtlem9  37782  prter2  37799  2llnmat  38443  2lnat  38703  cdlemefrs29bpre1  39316  elnn0rabdioph  41589  fiphp3d  41605  minregex  42333