Theorem epel 5558

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 5557	1 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145   class class class wbr 5103   E cep 5554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-eprel 5555

This theorem is used by:  epse  5637  dfepfr  5639  epfrc  5640  wecmpep  5647  wetrep  5648  dmep  5907  rnep  5911  xpdifcnvepel  6161  epweon  7774  epweonALT  7775  smoiso  8351  smoiso2  8358  ordunifi  9260  ordiso2  9487  ordtypelem8  9497  oismo  9512  wofib  9517  dford2  9599  noinfep  9639  oemapso  9661  wemapwe  9676  alephiso  10101  cflim2  10265  fin23lem27  10330  om2uzisoi  14018  om2noseqiso  28567  bnj219  35243  nummin  35598  efrunt  36292  dftr6  36330  dffr5  36333  elpotr  36358  dfon2lem9  36368  dfon2  36369  brsset  36466  dfon3  36469  brbigcup  36475  brapply  36515  brcup  36516  brcap  36517  dfint3  36531  dfssr2  39327  onsupuni  44070  onsupmaxb  44080  rankrelp  45783  sswfaxreg  45810  brpermmodel  45826  hashomiso  45848