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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

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

This theorem is referenced by:  nelb  3241  ceqsralv  3495  clel5  3625  reueq  3701  reuind  3717  0el  4319  reusv3  5378  elidinxp  6048  sucel  6439  fvmptt  7012  releldm2  8041  qsid  8780  ttrcltr  9686  zorng  10489  rereccl  11934  nndiv  12283  incexc2  15894  ruclem12  16298  chnfi  18691  conjnmzb  19324  pgpfac1lem2  20148  pgpfac1lem4  20151  mat1dimelbas  22609  mat1dimbas  22610  chmaidscmat  22986  unisngl  23665  fmid  24098  dcubic  26992  addsrid  28138  addsprop  28150  negsprop  28209  mulsrid  28287  mulsprop  28304  onsfi  28530  fusgrn0degnn0  29830  chscllem2  31971  disjunsn  32920  grplsm0l  33693  ballotlemsima  34887  dfon2lem8  36261  brimg  36408  dfrecs2  36423  altopelaltxp  36449  prtlem9  39619  prter2  39636  2llnmat  40279  2lnat  40539  cdlemefrs29bpre1  41152  elnn0rabdioph  43513  fiphp3d  43529  minregex  44243