Theorem epel 5553

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144   class class class wbr 5102   E cep 5549

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-eprel 5550

This theorem is used by:  epse  5632  dfepfr  5634  epfrc  5635  wecmpep  5642  wetrep  5643  dmep  5905  rnep  5909  xpdifcnvepel  6161  epweon  7791  epweonALT  7792  smoiso  8375  smoiso2  8382  ordunifi  9286  ordiso2  9514  ordtypelem8  9524  oismo  9539  wofib  9544  dford2  9626  noinfep  9666  oemapso  9688  wemapwe  9703  alephiso  10182  cflim2  10346  fin23lem27  10411  om2uzisoi  14102  om2noseqiso  28695  bnj219  35412  nummin  35776  efrunt  36572  dftr6  36610  dffr5  36613  elpotr  36637  dfon2lem9  36647  dfon2  36648  brsset  36745  dfon3  36748  brbigcup  36754  brapply  36794  brcup  36795  brcap  36796  dfint3  36810  dfssr2  39618  onsupuni  44338  onsupmaxb  44348  rankrelp  46057  sswfaxreg  46084  brpermmodel  46100  hashomiso  46122