Theorem risset 3207

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-rex 3057

This theorem is referenced by:  nelb  3208  ceqsralv  3477  clel5  3615  reueq  3691  reuind  3707  0el  4310  reusv3  5341  elidinxp  5992  sucel  6382  fvmptt  6949  releldm2  7975  qsid  8705  ttrcltr  9606  zorng  10395  rereccl  11839  nndiv  12171  incexc2  15745  ruclem12  16150  chnfi  18540  conjnmzb  19165  pgpfac1lem2  19989  pgpfac1lem4  19992  mat1dimelbas  22386  mat1dimbas  22387  chmaidscmat  22763  unisngl  23442  fmid  23875  dcubic  26783  addsrid  27907  addsprop  27919  negsprop  27977  mulsrid  28052  mulsprop  28069  onsfi  28283  fusgrn0degnn0  29478  chscllem2  31618  disjunsn  32574  grplsm0l  33368  ballotlemsima  34529  dfon2lem8  35832  brimg  35979  dfrecs2  35994  altopelaltxp  36020  prtlem9  38962  prter2  38979  2llnmat  39622  2lnat  39882  cdlemefrs29bpre1  40495  elnn0rabdioph  42895  fiphp3d  42911  minregex  43626