Theorem epel 5534

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114   class class class wbr 5085   E cep 5530

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-eprel 5531

This theorem is referenced by:  epse  5613  dfepfr  5615  epfrc  5616  wecmpep  5623  wetrep  5624  dmep  5878  rnep  5882  epweon  7729  epweonALT  7730  smoiso  8302  smoiso2  8309  ordunifi  9200  ordiso2  9430  ordtypelem8  9440  oismo  9455  wofib  9460  dford2  9541  noinfep  9581  oemapso  9603  wemapwe  9618  alephiso  10020  cflim2  10185  fin23lem27  10250  om2uzisoi  13916  om2noseqiso  28294  bnj219  34876  nummin  35236  efrunt  35895  dftr6  35933  dffr5  35936  elpotr  35961  dfon2lem9  35971  dfon2  35972  brsset  36069  dfon3  36072  brbigcup  36078  brapply  36118  brcup  36119  brcap  36120  dfint3  36134  dfssr2  38900  onsupuni  43657  onsupmaxb  43667  rankrelp  45387  sswfaxreg  45414  brpermmodel  45430