Theorem risset 3236

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 1880	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		dfclel 2837	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 306	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-rex 3086

This theorem is referenced by:  nelb  3237  ceqsralv  3493  clel5  3623  reueq  3698  reuind  3714  0el  4313  reusv3  5359  elidinxp  6029  sucel  6417  fvmptt  6991  releldm2  8019  qsid  8757  ttrcltr  9665  zorng  10455  rereccl  11903  nndiv  12253  incexc2  15859  ruclem12  16264  chnfi  18657  conjnmzb  19284  pgpfac1lem2  20108  pgpfac1lem4  20111  mat1dimelbas  22519  mat1dimbas  22520  chmaidscmat  22896  unisngl  23575  fmid  24008  dcubic  26899  addsrid  28045  addsprop  28057  negsprop  28116  mulsrid  28194  mulsprop  28211  onsfi  28437  fusgrn0degnn0  29657  chscllem2  31798  disjunsn  32754  grplsm0l  33550  ballotlemsima  34774  dfon2lem8  36099  brimg  36246  dfrecs2  36261  altopelaltxp  36287  prtlem9  39449  prter2  39466  2llnmat  40109  2lnat  40369  cdlemefrs29bpre1  40982  elnn0rabdioph  43341  fiphp3d  43357  minregex  44071