Theorem epel 5544

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   class class class wbr 5110   E cep 5540

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-eprel 5541

This theorem is referenced by:  epse  5623  dfepfr  5625  epfrc  5626  wecmpep  5633  wetrep  5634  dmep  5890  rnep  5893  epweon  7754  epweonALT  7755  smoiso  8334  smoiso2  8341  ordunifi  9244  ordiso2  9475  ordtypelem8  9485  oismo  9500  wofib  9505  dford2  9580  noinfep  9620  oemapso  9642  wemapwe  9657  alephiso  10058  cflim2  10223  fin23lem27  10288  om2uzisoi  13926  om2noseqiso  28203  bnj219  34730  nummin  35088  efrunt  35707  dftr6  35745  dffr5  35748  elpotr  35776  dfon2lem9  35786  dfon2  35787  brsset  35884  dfon3  35887  brbigcup  35893  brapply  35933  brcup  35934  brcap  35935  dfint3  35947  dfssr2  38497  onsupuni  43225  onsupmaxb  43235  rankrelp  44957  sswfaxreg  44984  brpermmodel  45000