Theorem epel 5489

Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. (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 3426	. 2 ⊢ 𝑥 ∈ V
2	1	epeli 5488	1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∈ wcel 2108   class class class wbr 5070   E cep 5485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-eprel 5486

This theorem is referenced by:  epse  5563  dfepfr  5565  epfrc  5566  wecmpep  5572  wetrep  5573  dmep  5821  domepOLD  5822  rnep  5825  epweon  7603  smoiso  8164  smoiso2  8171  ordunifi  8994  ordiso2  9204  ordtypelem8  9214  oismo  9229  wofib  9234  dford2  9308  noinfep  9348  oemapso  9370  wemapwe  9385  alephiso  9785  cflim2  9950  fin23lem27  10015  om2uzisoi  13602  bnj219  32612  nummin  32963  efrunt  33554  dftr6  33624  dffr5  33627  elpotr  33663  dfon2lem9  33673  dfon2  33674  brsset  34118  dfon3  34121  brbigcup  34127  brapply  34167  brcup  34168  brcap  34169  dfint3  34181  dfssr2  36544