Theorem epel 5564

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143   class class class wbr 5109   E cep 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-eprel 5561

This theorem is referenced by:  epse  5643  dfepfr  5645  epfrc  5646  wecmpep  5653  wetrep  5654  dmep  5913  rnep  5917  xpdifcnvepel  6166  epweon  7770  epweonALT  7771  smoiso  8345  smoiso2  8352  ordunifi  9246  ordiso2  9473  ordtypelem8  9483  oismo  9498  wofib  9503  dford2  9585  noinfep  9625  oemapso  9647  wemapwe  9662  alephiso  10078  cflim2  10242  fin23lem27  10307  om2uzisoi  13986  om2noseqiso  28495  bnj219  35122  nummin  35484  efrunt  36205  dftr6  36243  dffr5  36246  elpotr  36271  dfon2lem9  36281  dfon2  36282  brsset  36379  dfon3  36382  brbigcup  36388  brapply  36428  brcup  36429  brcap  36430  dfint3  36444  dfssr2  39228  onsupuni  43956  onsupmaxb  43966  rankrelp  45669  sswfaxreg  45696  brpermmodel  45712  hashomiso  45734