Theorem epel 5514

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111   class class class wbr 5086   E cep 5510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-eprel 5511

This theorem is referenced by:  epse  5593  dfepfr  5595  epfrc  5596  wecmpep  5603  wetrep  5604  dmep  5858  rnep  5862  epweon  7703  epweonALT  7704  smoiso  8277  smoiso2  8284  ordunifi  9169  ordiso2  9396  ordtypelem8  9406  oismo  9421  wofib  9426  dford2  9505  noinfep  9545  oemapso  9567  wemapwe  9582  alephiso  9984  cflim2  10149  fin23lem27  10214  om2uzisoi  13856  om2noseqiso  28227  bnj219  34737  nummin  35096  efrunt  35749  dftr6  35787  dffr5  35790  elpotr  35815  dfon2lem9  35825  dfon2  35826  brsset  35923  dfon3  35926  brbigcup  35932  brapply  35972  brcup  35973  brcap  35974  dfint3  35986  dfssr2  38536  onsupuni  43262  onsupmaxb  43272  rankrelp  44993  sswfaxreg  45020  brpermmodel  45036