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  4308  reusv3  5338  elidinxp  5988  sucel  6377  fvmptt  6944  releldm2  7970  qsid  8700  ttrcltr  9601  zorng  10390  rereccl  11834  nndiv  12166  incexc2  15740  ruclem12  16145  chnfi  18535  conjnmzb  19160  pgpfac1lem2  19984  pgpfac1lem4  19987  mat1dimelbas  22381  mat1dimbas  22382  chmaidscmat  22758  unisngl  23437  fmid  23870  dcubic  26778  addsrid  27902  addsprop  27914  negsprop  27972  mulsrid  28047  mulsprop  28064  onsfi  28278  fusgrn0degnn0  29473  chscllem2  31610  disjunsn  32566  grplsm0l  33360  ballotlemsima  34521  dfon2lem8  35824  brimg  35971  dfrecs2  35984  altopelaltxp  36010  prtlem9  38903  prter2  38920  2llnmat  39563  2lnat  39823  cdlemefrs29bpre1  40436  elnn0rabdioph  42836  fiphp3d  42852  minregex  43567