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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-rex 3069

This theorem is referenced by:  nelb  3232  nelbOLD  3233  ceqsralv  3520  clel5  3665  reueq  3746  reuind  3762  0el  4369  iunidOLD  5066  reusv3  5411  elidinxp  6064  sucel  6460  fvmptt  7036  releldm2  8067  qsid  8822  ttrcltr  9754  zorng  10542  rereccl  11983  nndiv  12310  incexc2  15871  ruclem12  16274  conjnmzb  19284  pgpfac1lem2  20110  pgpfac1lem4  20113  mat1dimelbas  22493  mat1dimbas  22494  chmaidscmat  22870  unisngl  23551  fmid  23984  dcubic  26904  addsrid  28012  addsprop  28024  negsprop  28082  mulsrid  28154  mulsprop  28171  fusgrn0degnn0  29532  chscllem2  31667  disjunsn  32614  grplsm0l  33411  ballotlemsima  34497  dfon2lem8  35772  brimg  35919  dfrecs2  35932  altopelaltxp  35958  prtlem9  38846  prter2  38863  2llnmat  39507  2lnat  39767  cdlemefrs29bpre1  40380  elnn0rabdioph  42791  fiphp3d  42807  minregex  43524