Theorem epel 5521

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119   class class class wbr 5072   E cep 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-eprel 5518

This theorem is referenced by:  epse  5600  dfepfr  5602  epfrc  5603  wecmpep  5610  wetrep  5611  dmep  5865  rnep  5869  epweon  7718  epweonALT  7719  smoiso  8292  smoiso2  8299  ordunifi  9190  ordiso2  9420  ordtypelem8  9430  oismo  9445  wofib  9450  dford2  9532  noinfep  9572  oemapso  9594  wemapwe  9609  alephiso  10011  cflim2  10176  fin23lem27  10241  om2uzisoi  13907  om2noseqiso  28312  bnj219  34916  nummin  35274  efrunt  35941  dftr6  35979  dffr5  35982  elpotr  36007  dfon2lem9  36017  dfon2  36018  brsset  36115  dfon3  36118  brbigcup  36124  brapply  36164  brcup  36165  brcap  36166  dfint3  36180  dfssr2  38946  onsupuni  43674  onsupmaxb  43684  rankrelp  45404  sswfaxreg  45431  brpermmodel  45447