Theorem risset 3247

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 1905	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 3096	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		df-clel 2774	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 296	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 198   ∧ wa 386   = wceq 1601  ∃wex 1823   ∈ wcel 2107  ∃wrex 3091

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-clel 2774  df-rex 3096

This theorem is referenced by:  clel5  3547  reueq  3618  reuind  3628  0el  4169  iunid  4810  reusv3  5119  elidinxp  5707  sucel  6051  fvmptt  6563  releldm2  7499  qsid  8098  zorng  9663  rereccl  11096  nndiv  11426  zqOLD  12107  incexc2  14983  ruclem12  15383  conjnmzb  18090  pgpfac1lem2  18872  pgpfac1lem4  18875  mat1dimelbas  20693  mat1dimbas  20694  chmaidscmat  21071  unisngl  21750  fmid  22183  dcubic  25035  fusgrn0degnn0  26864  chscllem2  29086  disjunsn  29987  ballotlemsima  31184  dfon2lem8  32291  brimg  32641  dfrecs2  32654  altopelaltxp  32680  prtlem9  35027  prtlem11  35029  prter2  35044  2llnmat  35687  2lnat  35947  cdlemefrs29bpre1  36560  elnn0rabdioph  38341  fiphp3d  38357