Theorem epel 5561

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147   class class class wbr 5108   E cep 5557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-eprel 5558

This theorem is used by:  epse  5640  dfepfr  5642  epfrc  5643  wecmpep  5650  wetrep  5651  dmep  5917  rnep  5921  xpdifcnvepel  6178  epweon  7821  epweonALT  7822  smoiso  8408  smoiso2  8415  ordunifi  9319  ordiso2  9546  ordtypelem8  9556  oismo  9571  wofib  9576  dford2  9658  noinfep  9698  oemapso  9720  wemapwe  9735  alephiso  10216  cflim2  10380  fin23lem27  10445  om2uzisoi  14137  om2noseqiso  28745  bnj219  35475  nummin  35847  efrunt  36693  dftr6  36731  dffr5  36734  elpotr  36758  dfon2lem9  36768  dfon2  36769  brsset  36866  dfon3  36869  brbigcup  36875  brapply  36915  brcup  36916  brcap  36917  dfint3  36931  dfssr2  39777  onsupuni  44492  onsupmaxb  44502  rankrelp  46214  sswfaxreg  46241  brpermmodel  46257  hashomiso  46279