Theorem epel 5580

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

Syntax hints:   ↔ wb 205   ∈ wcel 2099   class class class wbr 5143   E cep 5576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-eprel 5577

This theorem is referenced by:  epse  5656  dfepfr  5658  epfrc  5659  wecmpep  5665  wetrep  5666  dmep  5921  rnep  5924  epweon  7772  epweonALT  7773  smoiso  8377  smoiso2  8384  ordunifi  9312  ordiso2  9533  ordtypelem8  9543  oismo  9558  wofib  9563  dford2  9638  noinfep  9678  oemapso  9700  wemapwe  9715  alephiso  10116  cflim2  10281  fin23lem27  10346  om2uzisoi  13946  om2noseqiso  28169  bnj219  34359  nummin  34709  efrunt  35302  dftr6  35340  dffr5  35343  elpotr  35372  dfon2lem9  35382  dfon2  35383  brsset  35480  dfon3  35483  brbigcup  35489  brapply  35529  brcup  35530  brcap  35531  dfint3  35543  dfssr2  37966  onsupuni  42648  onsupmaxb  42658

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »