Theorem risset 3229

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∃wrex 3069

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 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-clel 2809  df-rex 3070

This theorem is referenced by:  nelb  3230  nelbOLD  3231  ceqsralv  3513  clel5  3655  reueq  3733  reuind  3749  0el  4360  iunidOLD  5064  reusv3  5403  elidinxp  6043  sucel  6438  fvmptt  7018  releldm2  8033  qsid  8783  ttrcltr  9717  zorng  10505  rereccl  11939  nndiv  12265  incexc2  15791  ruclem12  16191  conjnmzb  19174  pgpfac1lem2  19993  pgpfac1lem4  19996  mat1dimelbas  22293  mat1dimbas  22294  chmaidscmat  22670  unisngl  23351  fmid  23784  dcubic  26692  addsrid  27794  addsprop  27806  negsprop  27860  mulsrid  27926  mulsprop  27943  fusgrn0degnn0  29189  chscllem2  31324  disjunsn  32258  grplsm0l  32953  ballotlemsima  33978  dfon2lem8  35232  brimg  35379  dfrecs2  35392  altopelaltxp  35418  prtlem9  38198  prter2  38215  2llnmat  38859  2lnat  39119  cdlemefrs29bpre1  39732  elnn0rabdioph  42004  fiphp3d  42020  minregex  42748