MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  epse Structured version   Visualization version   GIF version

Theorem epse 5573
Description: The membership relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the membership relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
Assertion
Ref Expression
epse E Se 𝐴

Proof of Theorem epse
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 epel 5499 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
21bicomi 223 . . . . . 6 (𝑦𝑥𝑦 E 𝑥)
32abbi2i 2880 . . . . 5 𝑥 = {𝑦𝑦 E 𝑥}
4 vex 3437 . . . . 5 𝑥 ∈ V
53, 4eqeltrri 2837 . . . 4 {𝑦𝑦 E 𝑥} ∈ V
6 rabssab 4019 . . . 4 {𝑦𝐴𝑦 E 𝑥} ⊆ {𝑦𝑦 E 𝑥}
75, 6ssexi 5247 . . 3 {𝑦𝐴𝑦 E 𝑥} ∈ V
87rgenw 3077 . 2 𝑥𝐴 {𝑦𝐴𝑦 E 𝑥} ∈ V
9 df-se 5546 . 2 ( E Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦 E 𝑥} ∈ V)
108, 9mpbir 230 1 E Se 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {cab 2716  wral 3065  {crab 3069  Vcvv 3433   class class class wbr 5075   E cep 5495   Se wse 5543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-eprel 5496  df-se 5546
This theorem is referenced by:  omsinds  7742  omsindsOLD  7743  tfr1ALT  8240  tfr2ALT  8241  tfr3ALT  8242  oieu  9307  oismo  9308  oiid  9309  cantnfp1lem3  9447  r0weon  9777  hsmexlem1  10191  on2recsfn  33835  on2recsov  33836  on2ind  33837  on3ind  33838
  Copyright terms: Public domain W3C validator