Theorem risset 3215

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 1868	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2816	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 305	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-rex 3065

This theorem is referenced by:  nelb  3216  ceqsralv  3473  clel5  3610  reueq  3685  reuind  3701  0el  4298  reusv3  5341  elidinxp  6003  sucel  6393  fvmptt  6963  releldm2  7992  qsid  8725  ttrcltr  9635  zorng  10424  rereccl  11871  nndiv  12221  incexc2  15801  ruclem12  16206  chnfi  18598  conjnmzb  19226  pgpfac1lem2  20050  pgpfac1lem4  20053  mat1dimelbas  22461  mat1dimbas  22462  chmaidscmat  22838  unisngl  23517  fmid  23950  dcubic  26835  addsrid  27981  addsprop  27993  negsprop  28052  mulsrid  28130  mulsprop  28147  onsfi  28373  fusgrn0degnn0  29593  chscllem2  31734  disjunsn  32690  grplsm0l  33493  ballotlemsima  34707  dfon2lem8  36023  brimg  36170  dfrecs2  36185  altopelaltxp  36211  prtlem9  39363  prter2  39380  2llnmat  40023  2lnat  40283  cdlemefrs29bpre1  40896  elnn0rabdioph  43255  fiphp3d  43271  minregex  43985