Theorem risset 3212

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-rex 3054

This theorem is referenced by:  nelb  3213  ceqsralv  3488  clel5  3631  reueq  3708  reuind  3724  0el  4326  iunidOLD  5025  reusv3  5360  elidinxp  6015  sucel  6408  fvmptt  6988  releldm2  8022  qsid  8754  ttrcltr  9669  zorng  10457  rereccl  11900  nndiv  12232  incexc2  15804  ruclem12  16209  conjnmzb  19185  pgpfac1lem2  20007  pgpfac1lem4  20010  mat1dimelbas  22358  mat1dimbas  22359  chmaidscmat  22735  unisngl  23414  fmid  23847  dcubic  26756  addsrid  27871  addsprop  27883  negsprop  27941  mulsrid  28016  mulsprop  28033  onsfi  28247  fusgrn0degnn0  29427  chscllem2  31567  disjunsn  32523  grplsm0l  33374  ballotlemsima  34507  dfon2lem8  35778  brimg  35925  dfrecs2  35938  altopelaltxp  35964  prtlem9  38857  prter2  38874  2llnmat  39518  2lnat  39778  cdlemefrs29bpre1  40391  elnn0rabdioph  42791  fiphp3d  42807  minregex  43523