Theorem epel 5566

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146   class class class wbr 5111   E cep 5562

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-eprel 5563

This theorem is used by:  epse  5645  dfepfr  5647  epfrc  5648  wecmpep  5655  wetrep  5656  dmep  5915  rnep  5919  xpdifcnvepel  6168  epweon  7780  epweonALT  7781  smoiso  8355  smoiso2  8362  ordunifi  9257  ordiso2  9484  ordtypelem8  9494  oismo  9509  wofib  9514  dford2  9596  noinfep  9636  oemapso  9658  wemapwe  9673  alephiso  10098  cflim2  10262  fin23lem27  10327  om2uzisoi  14008  om2noseqiso  28546  bnj219  35187  nummin  35542  efrunt  36242  dftr6  36280  dffr5  36283  elpotr  36308  dfon2lem9  36318  dfon2  36319  brsset  36416  dfon3  36419  brbigcup  36425  brapply  36465  brcup  36466  brcap  36467  dfint3  36481  dfssr2  39286  onsupuni  44014  onsupmaxb  44024  rankrelp  45727  sswfaxreg  45754  brpermmodel  45770  hashomiso  45792