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

Syntax hints:   ↔ wb 206   ∈ wcel 2113   class class class wbr 5098   E cep 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-eprel 5524

This theorem is referenced by:  epse  5606  dfepfr  5608  epfrc  5609  wecmpep  5616  wetrep  5617  dmep  5872  rnep  5876  epweon  7720  epweonALT  7721  smoiso  8294  smoiso2  8301  ordunifi  9190  ordiso2  9420  ordtypelem8  9430  oismo  9445  wofib  9450  dford2  9529  noinfep  9569  oemapso  9591  wemapwe  9606  alephiso  10008  cflim2  10173  fin23lem27  10238  om2uzisoi  13877  om2noseqiso  28298  bnj219  34889  nummin  35249  efrunt  35907  dftr6  35945  dffr5  35948  elpotr  35973  dfon2lem9  35983  dfon2  35984  brsset  36081  dfon3  36084  brbigcup  36090  brapply  36130  brcup  36131  brcap  36132  dfint3  36146  dfssr2  38752  onsupuni  43471  onsupmaxb  43481  rankrelp  45201  sswfaxreg  45228  brpermmodel  45244