Theorem epel 5546

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141   class class class wbr 5097   E cep 5542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-eprel 5543

This theorem is referenced by:  epse  5625  dfepfr  5627  epfrc  5628  wecmpep  5635  wetrep  5636  dmep  5895  rnep  5899  epweon  7753  epweonALT  7754  smoiso  8327  smoiso2  8334  ordunifi  9228  ordiso2  9457  ordtypelem8  9467  oismo  9482  wofib  9487  dford2  9569  noinfep  9609  oemapso  9631  wemapwe  9646  alephiso  10048  cflim2  10214  fin23lem27  10279  om2uzisoi  13961  om2noseqiso  28383  bnj219  34990  nummin  35350  efrunt  36024  dftr6  36062  dffr5  36065  elpotr  36090  dfon2lem9  36100  dfon2  36101  brsset  36198  dfon3  36201  brbigcup  36207  brapply  36247  brcup  36248  brcap  36249  dfint3  36263  dfssr2  39039  onsupuni  43767  onsupmaxb  43777  rankrelp  45497  sswfaxreg  45524  brpermmodel  45540