Theorem epel 5499

Description: The membership relation and the membership predicate agree when the "containing" class is a setvar. (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 3437	. 2 ⊢ 𝑥 ∈ V
2	1	epeli 5498	1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)

Syntax hints:   ↔ wb 205   ∈ wcel 2107   class class class wbr 5075   E cep 5495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-eprel 5496

This theorem is referenced by:  epse  5573  dfepfr  5575  epfrc  5576  wecmpep  5582  wetrep  5583  dmep  5835  domepOLD  5836  rnep  5839  epweon  7634  epweonOLD  7635  smoiso  8202  smoiso2  8209  ordunifi  9073  ordiso2  9283  ordtypelem8  9293  oismo  9308  wofib  9313  dford2  9387  noinfep  9427  oemapso  9449  wemapwe  9464  alephiso  9863  cflim2  10028  fin23lem27  10093  om2uzisoi  13683  bnj219  32721  nummin  33072  efrunt  33663  dftr6  33727  dffr5  33730  elpotr  33766  dfon2lem9  33776  dfon2  33777  brsset  34200  dfon3  34203  brbigcup  34209  brapply  34249  brcup  34250  brcap  34251  dfint3  34263  dfssr2  36624