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  27448  addsprop  27460  negsprop  27509  mulsrid  27569  mulsprop  27586  fusgrn0degnn0  28756  chscllem2  30891  disjunsn  31825  grplsm0l  32513  ballotlemsima  33514  dfon2lem8  34762  brimg  34909  dfrecs2  34922  altopelaltxp  34948  prtlem9  37734  prter2  37751  2llnmat  38395  2lnat  38655  cdlemefrs29bpre1  39268  elnn0rabdioph  41541  fiphp3d  41557  minregex  42285