Theorem epel 5527

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114   class class class wbr 5086   E cep 5523

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 2709  ax-sep 5231  ax-pr 5370

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-eprel 5524

This theorem is referenced by:  epse  5606  dfepfr  5608  epfrc  5609  wecmpep  5616  wetrep  5617  dmep  5872  rnep  5876  epweon  7722  epweonALT  7723  smoiso  8295  smoiso2  8302  ordunifi  9193  ordiso2  9423  ordtypelem8  9433  oismo  9448  wofib  9453  dford2  9532  noinfep  9572  oemapso  9594  wemapwe  9609  alephiso  10011  cflim2  10176  fin23lem27  10241  om2uzisoi  13907  om2noseqiso  28308  bnj219  34892  nummin  35252  efrunt  35911  dftr6  35949  dffr5  35952  elpotr  35977  dfon2lem9  35987  dfon2  35988  brsset  36085  dfon3  36088  brbigcup  36094  brapply  36134  brcup  36135  brcap  36136  dfint3  36150  dfssr2  38914  onsupuni  43675  onsupmaxb  43685  rankrelp  45405  sswfaxreg  45432  brpermmodel  45448