Theorem epel 5534

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102   E cep 5530

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-eprel 5531

This theorem is referenced by:  epse  5613  dfepfr  5615  epfrc  5616  wecmpep  5623  wetrep  5624  dmep  5877  rnep  5880  epweon  7731  epweonALT  7732  smoiso  8308  smoiso2  8315  ordunifi  9213  ordiso2  9444  ordtypelem8  9454  oismo  9469  wofib  9474  dford2  9549  noinfep  9589  oemapso  9611  wemapwe  9626  alephiso  10027  cflim2  10192  fin23lem27  10257  om2uzisoi  13895  om2noseqiso  28172  bnj219  34696  nummin  35054  efrunt  35673  dftr6  35711  dffr5  35714  elpotr  35742  dfon2lem9  35752  dfon2  35753  brsset  35850  dfon3  35853  brbigcup  35859  brapply  35899  brcup  35900  brcap  35901  dfint3  35913  dfssr2  38463  onsupuni  43191  onsupmaxb  43201  rankrelp  44923  sswfaxreg  44950  brpermmodel  44966