Theorem risset 3240

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-rex 3090

This theorem is referenced by:  nelb  3241  ceqsralv  3497  clel5  3627  reueq  3703  reuind  3719  0el  4319  reusv3  5367  elidinxp  6037  sucel  6426  fvmptt  7000  releldm2  8028  qsid  8767  ttrcltr  9673  zorng  10476  rereccl  11924  nndiv  12273  incexc2  15882  ruclem12  16287  chnfi  18680  conjnmzb  19314  pgpfac1lem2  20138  pgpfac1lem4  20141  mat1dimelbas  22589  mat1dimbas  22590  chmaidscmat  22966  unisngl  23645  fmid  24078  dcubic  26969  addsrid  28115  addsprop  28127  negsprop  28186  mulsrid  28264  mulsprop  28281  onsfi  28507  fusgrn0degnn0  29758  chscllem2  31899  disjunsn  32849  grplsm0l  33628  ballotlemsima  34823  dfon2lem8  36151  brimg  36298  dfrecs2  36313  altopelaltxp  36339  prtlem9  39500  prter2  39517  2llnmat  40160  2lnat  40420  cdlemefrs29bpre1  41033  elnn0rabdioph  43392  fiphp3d  43408  minregex  44122