Theorem epel 5554

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  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 5551

This theorem is used by:  epse  5633  dfepfr  5635  epfrc  5636  wecmpep  5643  wetrep  5644  dmep  5905  rnep  5909  xpdifcnvepel  6160  epweon  7787  epweonALT  7788  smoiso  8363  smoiso2  8370  ordunifi  9274  ordiso2  9502  ordtypelem8  9512  oismo  9527  wofib  9532  dford2  9614  noinfep  9654  oemapso  9676  wemapwe  9691  alephiso  10170  cflim2  10334  fin23lem27  10399  om2uzisoi  14090  om2noseqiso  28681  bnj219  35357  nummin  35711  efrunt  36457  dftr6  36495  dffr5  36498  elpotr  36523  dfon2lem9  36533  dfon2  36534  brsset  36631  dfon3  36634  brbigcup  36640  brapply  36680  brcup  36681  brcap  36682  dfint3  36696  dfssr2  39491  onsupuni  44215  onsupmaxb  44225  rankrelp  45928  sswfaxreg  45955  brpermmodel  45971  hashomiso  45993