Theorem epel 4952

Description: The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
epel	⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)

Proof of Theorem epel

Step	Hyp	Ref	Expression
1		vex 3176	. 2 ⊢ 𝑦 ∈ V
2	1	epelc 4951	1 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)

Syntax hints:   ↔ wb 195   class class class wbr 4583   E cep 4947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-eprel 4949

This theorem is referenced by:  epse  5021  dfepfr  5023  epfrc  5024  wecmpep  5030  wetrep  5031  ordon  6874  smoiso  7346  smoiso2  7353  ordunifi  8095  ordiso2  8303  ordtypelem8  8313  wofib  8333  dford2  8400  noinfep  8440  oemapso  8462  wemapwe  8477  alephiso  8804  cflim2  8968  fin23lem27  9033  om2uzisoi  12615  bnj219  30055  efrunt  30844  dftr6  30893  dffr5  30896  elpotr  30930  dfon2lem9  30940  dfon2  30941  domep  30942  brsset  31166  dfon3  31169  brbigcup  31175  brapply  31215  brcup  31216  brcap  31217  dfint3  31229