Theorem epel 5582

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 3478	. 2 ⊢ 𝑥 ∈ V
2	1	epeli 5581	1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∈ wcel 2106   class class class wbr 5147   E cep 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-eprel 5579

This theorem is referenced by:  epse  5658  dfepfr  5660  epfrc  5661  wecmpep  5667  wetrep  5668  dmep  5921  rnep  5924  epweon  7758  epweonALT  7759  smoiso  8358  smoiso2  8365  ordunifi  9289  ordiso2  9506  ordtypelem8  9516  oismo  9531  wofib  9536  dford2  9611  noinfep  9651  oemapso  9673  wemapwe  9688  alephiso  10089  cflim2  10254  fin23lem27  10319  om2uzisoi  13915  bnj219  33732  nummin  34082  efrunt  34670  dftr6  34709  dffr5  34712  elpotr  34741  dfon2lem9  34751  dfon2  34752  brsset  34849  dfon3  34852  brbigcup  34858  brapply  34898  brcup  34899  brcap  34900  dfint3  34912  dfssr2  37357  onsupuni  41963  onsupmaxb  41973