Theorem risset 3241

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-rex 3091

This theorem is used by:  nelb  3242  ceqsralv  3494  clel5  3622  reueq  3698  reuind  3714  0el  4314  reusv3  5374  elidinxp  6054  sucel  6465  fvmptt  7045  releldm2  8088  qsid  8840  ttrcltr  9754  zorng  10621  rereccl  12075  nndiv  12424  incexc2  16051  ruclem12  16453  chnfi  18858  conjnmzb  19517  pgpfac1lem2  20342  pgpfac1lem4  20345  mat1dimelbas  22841  mat1dimbas  22842  chmaidscmat  23221  unisngl  23901  fmid  24334  dcubic  27231  addsrid  28407  addsprop  28419  negsprop  28478  mulsrid  28556  mulsprop  28573  onsfi  28799  fusgrn0degnn0  30137  chscllem2  32297  disjunsn  33286  grplsm0l  34058  ballotlemsima  35259  dfon2lem8  36767  brimg  36914  dfrecs2  36929  altopelaltxp  36956  prtlem9  40187  prter2  40204  2llnmat  40847  2lnat  41107  cdlemefrs29bpre1  41720  elnn0rabdioph  44076  fiphp3d  44092  minregex  44796