Theorem epel 5541

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109   class class class wbr 5107   E cep 5537

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-eprel 5538

This theorem is referenced by:  epse  5620  dfepfr  5622  epfrc  5623  wecmpep  5630  wetrep  5631  dmep  5887  rnep  5890  epweon  7751  epweonALT  7752  smoiso  8331  smoiso2  8338  ordunifi  9237  ordiso2  9468  ordtypelem8  9478  oismo  9493  wofib  9498  dford2  9573  noinfep  9613  oemapso  9635  wemapwe  9650  alephiso  10051  cflim2  10216  fin23lem27  10281  om2uzisoi  13919  om2noseqiso  28196  bnj219  34723  nummin  35081  efrunt  35700  dftr6  35738  dffr5  35741  elpotr  35769  dfon2lem9  35779  dfon2  35780  brsset  35877  dfon3  35880  brbigcup  35886  brapply  35926  brcup  35927  brcap  35928  dfint3  35940  dfssr2  38490  onsupuni  43218  onsupmaxb  43228  rankrelp  44950  sswfaxreg  44977  brpermmodel  44993