Theorem risset 3239

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-rex 3077

This theorem is referenced by:  nelb  3240  nelbOLD  3241  ceqsralv  3531  clel5  3678  reueq  3759  reuind  3775  0el  4386  iunidOLD  5084  reusv3  5423  elidinxp  6073  sucel  6469  fvmptt  7049  releldm2  8084  qsid  8841  ttrcltr  9785  zorng  10573  rereccl  12012  nndiv  12339  incexc2  15886  ruclem12  16289  conjnmzb  19293  pgpfac1lem2  20119  pgpfac1lem4  20122  mat1dimelbas  22498  mat1dimbas  22499  chmaidscmat  22875  unisngl  23556  fmid  23989  dcubic  26907  addsrid  28015  addsprop  28027  negsprop  28085  mulsrid  28157  mulsprop  28174  fusgrn0degnn0  29535  chscllem2  31670  disjunsn  32616  grplsm0l  33396  ballotlemsima  34480  dfon2lem8  35754  brimg  35901  dfrecs2  35914  altopelaltxp  35940  prtlem9  38820  prter2  38837  2llnmat  39481  2lnat  39741  cdlemefrs29bpre1  40354  elnn0rabdioph  42759  fiphp3d  42775  minregex  43496