Theorem risset 3044

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 1774	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
2		df-rex 2902	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴))
3		df-clel 2606	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
4	1, 2, 3	3bitr4ri 292	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴)

Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-clel 2606  df-rex 2902

This theorem is referenced by:  reueq  3371  reuind  3378  0el  3895  iunid  4511  reusv3  4802  sucel  5715  fvmptt  6208  releldm2  7109  qsid  7700  zorng  9209  rereccl  10622  nndiv  10938  zq  11670  4fvwrd4  12328  wrdlen1  13198  incexc2  14409  ruclem12  14809  phisum  15333  conjnmzb  17518  symgmov1  17635  pgpfac1lem2  18297  pgpfac1lem4  18300  mat1dimelbas  20096  mat1dimbas  20097  chmaidscmat  20472  unisngl  21140  fmid  21574  dcubic  24373  usgn0fidegnn0  26556  chscllem2  27881  disjunsn  28789  ballotlemsima  29904  dfon2lem8  30939  brimg  31214  dfrecs2  31227  altopelaltxp  31253  prtlem9  33167  prtlem11  33169  prter2  33184  2llnmat  33828  2lnat  34088  cdlemefrs29bpre1  34703  elnn0rabdioph  36385  fiphp3d  36401  fusgrn0degnn0  40714