Theorem epel 5524

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113   class class class wbr 5095   E cep 5520

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 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-eprel 5521

This theorem is referenced by:  epse  5603  dfepfr  5605  epfrc  5606  wecmpep  5613  wetrep  5614  dmep  5869  rnep  5873  epweon  7717  epweonALT  7718  smoiso  8291  smoiso2  8298  ordunifi  9185  ordiso2  9412  ordtypelem8  9422  oismo  9437  wofib  9442  dford2  9521  noinfep  9561  oemapso  9583  wemapwe  9598  alephiso  10000  cflim2  10165  fin23lem27  10230  om2uzisoi  13868  om2noseqiso  28252  bnj219  34817  nummin  35176  efrunt  35829  dftr6  35867  dffr5  35870  elpotr  35895  dfon2lem9  35905  dfon2  35906  brsset  36003  dfon3  36006  brbigcup  36012  brapply  36052  brcup  36053  brcap  36054  dfint3  36068  dfssr2  38664  onsupuni  43386  onsupmaxb  43396  rankrelp  45117  sswfaxreg  45144  brpermmodel  45160