Theorem risset 3232

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2815  df-rex 3070

This theorem is referenced by:  nelb  3233  nelbOLD  3234  ceqsralv  3521  clel5  3664  reueq  3742  reuind  3758  0el  4362  iunidOLD  5060  reusv3  5404  elidinxp  6061  sucel  6457  fvmptt  7035  releldm2  8069  qsid  8824  ttrcltr  9757  zorng  10545  rereccl  11986  nndiv  12313  incexc2  15875  ruclem12  16278  conjnmzb  19272  pgpfac1lem2  20096  pgpfac1lem4  20099  mat1dimelbas  22478  mat1dimbas  22479  chmaidscmat  22855  unisngl  23536  fmid  23969  dcubic  26890  addsrid  27998  addsprop  28010  negsprop  28068  mulsrid  28140  mulsprop  28157  fusgrn0degnn0  29518  chscllem2  31658  disjunsn  32608  grplsm0l  33432  ballotlemsima  34519  dfon2lem8  35792  brimg  35939  dfrecs2  35952  altopelaltxp  35978  prtlem9  38866  prter2  38883  2llnmat  39527  2lnat  39787  cdlemefrs29bpre1  40400  elnn0rabdioph  42819  fiphp3d  42835  minregex  43552