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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-rex 3062

This theorem is referenced by:  nelb  3213  ceqsralv  3470  clel5  3607  reueq  3683  reuind  3699  0el  4303  reusv3  5347  elidinxp  6009  sucel  6399  fvmptt  6968  releldm2  7996  qsid  8728  ttrcltr  9637  zorng  10426  rereccl  11873  nndiv  12223  incexc2  15803  ruclem12  16208  chnfi  18600  conjnmzb  19228  pgpfac1lem2  20052  pgpfac1lem4  20055  mat1dimelbas  22436  mat1dimbas  22437  chmaidscmat  22813  unisngl  23492  fmid  23925  dcubic  26810  addsrid  27956  addsprop  27968  negsprop  28027  mulsrid  28105  mulsprop  28122  onsfi  28348  fusgrn0degnn0  29568  chscllem2  31709  disjunsn  32664  grplsm0l  33463  ballotlemsima  34660  dfon2lem8  35970  brimg  36117  dfrecs2  36132  altopelaltxp  36158  prtlem9  39310  prter2  39327  2llnmat  39970  2lnat  40230  cdlemefrs29bpre1  40843  elnn0rabdioph  43231  fiphp3d  43247  minregex  43961