Theorem risset 3237

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 1893	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2836	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 307	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-rex 3087

This theorem is used by:  nelb  3238  ceqsralv  3490  clel5  3618  reueq  3694  reuind  3710  0el  4310  reusv3  5366  elidinxp  6035  sucel  6439  fvmptt  7015  releldm2  8055  qsid  8806  ttrcltr  9721  zorng  10586  rereccl  12039  nndiv  12388  incexc2  16013  ruclem12  16415  chnfi  18814  conjnmzb  19473  pgpfac1lem2  20297  pgpfac1lem4  20300  mat1dimelbas  22792  mat1dimbas  22793  chmaidscmat  23172  unisngl  23852  fmid  24285  dcubic  27180  addsrid  28356  addsprop  28368  negsprop  28427  mulsrid  28505  mulsprop  28522  onsfi  28748  fusgrn0degnn0  30086  chscllem2  32246  disjunsn  33236  grplsm0l  34001  ballotlemsima  35195  dfon2lem8  36645  brimg  36792  dfrecs2  36807  altopelaltxp  36834  prtlem9  40015  prter2  40032  2llnmat  40675  2lnat  40935  cdlemefrs29bpre1  41548  elnn0rabdioph  43904  fiphp3d  43920  minregex  44629