Theorem risset 3062

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 1787	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 2918	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		df-clel 2618	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 293	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-clel 2618  df-rex 2918

This theorem is referenced by:  reueq  3404  reuind  3411  0el  3939  iunid  4575  reusv3  4876  sucel  5798  fvmptt  6300  releldm2  7218  qsid  7813  zorng  9326  rereccl  10743  nndiv  11061  zq  11794  4fvwrd4  12459  wrdlen1  13343  incexc2  14570  ruclem12  14970  phisum  15495  conjnmzb  17695  symgmov1  17812  pgpfac1lem2  18474  pgpfac1lem4  18477  mat1dimelbas  20277  mat1dimbas  20278  chmaidscmat  20653  unisngl  21330  fmid  21764  dcubic  24573  fusgrn0degnn0  26395  chscllem2  28497  disjunsn  29407  ballotlemsima  30577  dfon2lem8  31695  brimg  32044  dfrecs2  32057  altopelaltxp  32083  prtlem9  34149  prtlem11  34151  prter2  34166  2llnmat  34810  2lnat  35070  cdlemefrs29bpre1  35685  elnn0rabdioph  37367  fiphp3d  37383