Theorem risset 3213

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

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

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 2812  df-rex 3063

This theorem is referenced by:  nelb  3214  ceqsralv  3483  clel5  3621  reueq  3697  reuind  3713  0el  4317  reusv3  5352  elidinxp  6011  sucel  6401  fvmptt  6970  releldm2  7997  qsid  8730  ttrcltr  9637  zorng  10426  rereccl  11871  nndiv  12203  incexc2  15773  ruclem12  16178  chnfi  18569  conjnmzb  19194  pgpfac1lem2  20018  pgpfac1lem4  20021  mat1dimelbas  22427  mat1dimbas  22428  chmaidscmat  22804  unisngl  23483  fmid  23916  dcubic  26824  addsrid  27972  addsprop  27984  negsprop  28043  mulsrid  28121  mulsprop  28138  onsfi  28364  fusgrn0degnn0  29585  chscllem2  31725  disjunsn  32680  grplsm0l  33495  ballotlemsima  34693  dfon2lem8  36001  brimg  36148  dfrecs2  36163  altopelaltxp  36189  prtlem9  39237  prter2  39254  2llnmat  39897  2lnat  40157  cdlemefrs29bpre1  40770  elnn0rabdioph  43157  fiphp3d  43173  minregex  43887