Theorem epel 5587

Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. Definition 1.6 of [Schloeder] p. 1. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.)

Assertion

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

Proof of Theorem epel

Step	Hyp	Ref	Expression
1		vex 3484	. 2 ⊢ 𝑥 ∈ V
2	1	epeli 5586	1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 206   ∈ wcel 2108   class class class wbr 5143   E cep 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-eprel 5584

This theorem is referenced by:  epse  5667  dfepfr  5669  epfrc  5670  wecmpep  5677  wetrep  5678  dmep  5934  rnep  5937  epweon  7795  epweonALT  7796  smoiso  8402  smoiso2  8409  ordunifi  9326  ordiso2  9555  ordtypelem8  9565  oismo  9580  wofib  9585  dford2  9660  noinfep  9700  oemapso  9722  wemapwe  9737  alephiso  10138  cflim2  10303  fin23lem27  10368  om2uzisoi  13995  om2noseqiso  28308  bnj219  34747  nummin  35105  efrunt  35713  dftr6  35751  dffr5  35754  elpotr  35782  dfon2lem9  35792  dfon2  35793  brsset  35890  dfon3  35893  brbigcup  35899  brapply  35939  brcup  35940  brcap  35941  dfint3  35953  dfssr2  38500  onsupuni  43241  onsupmaxb  43251  rankrelp  44977  sswfaxreg  45004