Theorem epel 5522

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   class class class wbr 5092   E cep 5518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-eprel 5519

This theorem is referenced by:  epse  5601  dfepfr  5603  epfrc  5604  wecmpep  5611  wetrep  5612  dmep  5866  rnep  5869  epweon  7711  epweonALT  7712  smoiso  8285  smoiso2  8292  ordunifi  9179  ordiso2  9407  ordtypelem8  9417  oismo  9432  wofib  9437  dford2  9516  noinfep  9556  oemapso  9578  wemapwe  9593  alephiso  9992  cflim2  10157  fin23lem27  10222  om2uzisoi  13861  om2noseqiso  28201  bnj219  34700  nummin  35058  efrunt  35686  dftr6  35724  dffr5  35727  elpotr  35755  dfon2lem9  35765  dfon2  35766  brsset  35863  dfon3  35866  brbigcup  35872  brapply  35912  brcup  35913  brcap  35914  dfint3  35926  dfssr2  38476  onsupuni  43202  onsupmaxb  43212  rankrelp  44934  sswfaxreg  44961  brpermmodel  44977