Theorem epel 5556

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108   class class class wbr 5119   E cep 5552

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-eprel 5553

This theorem is referenced by:  epse  5636  dfepfr  5638  epfrc  5639  wecmpep  5646  wetrep  5647  dmep  5903  rnep  5906  epweon  7769  epweonALT  7770  smoiso  8376  smoiso2  8383  ordunifi  9298  ordiso2  9529  ordtypelem8  9539  oismo  9554  wofib  9559  dford2  9634  noinfep  9674  oemapso  9696  wemapwe  9711  alephiso  10112  cflim2  10277  fin23lem27  10342  om2uzisoi  13972  om2noseqiso  28248  bnj219  34764  nummin  35122  efrunt  35730  dftr6  35768  dffr5  35771  elpotr  35799  dfon2lem9  35809  dfon2  35810  brsset  35907  dfon3  35910  brbigcup  35916  brapply  35956  brcup  35957  brcap  35958  dfint3  35970  dfssr2  38517  onsupuni  43253  onsupmaxb  43263  rankrelp  44985  sswfaxreg  45012  brpermmodel  45028