ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssel Structured version   GIF version

Theorem ssel 2910
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssel (AB → (𝐶 A𝐶 B))

Proof of Theorem ssel
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 dfss2 2905 . . . . . 6 (ABx(x Ax B))
21biimpi 113 . . . . 5 (ABx(x Ax B))
3219.21bi 1426 . . . 4 (AB → (x Ax B))
43anim2d 320 . . 3 (AB → ((x = 𝐶 x A) → (x = 𝐶 x B)))
54eximdv 1736 . 2 (AB → (x(x = 𝐶 x A) → x(x = 𝐶 x B)))
6 df-clel 2012 . 2 (𝐶 Ax(x = 𝐶 x A))
7 df-clel 2012 . 2 (𝐶 Bx(x = 𝐶 x B))
85, 6, 73imtr4g 194 1 (AB → (𝐶 A𝐶 B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wal 1224   = wceq 1226  wex 1357   wcel 1369  wss 2888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-11 1373  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1622  df-clab 2003  df-cleq 2009  df-clel 2012  df-in 2895  df-ss 2902
This theorem is referenced by:  ssel2  2911  sseli  2912  sseld  2915  sstr2  2923  ssralv  2975  ssrexv  2976  ralss  2977  rexss  2978  ssconb  3047  sscon  3048  ssdif  3049  unss1  3083  ssrin  3133  difin2  3170  reuss2  3188  reupick  3192  sssnm  3491  uniss  3567  ss2iun  3638  ssiun  3665  iinss  3674  disjss2  3714  disjss1  3717  pwnss  3878  sspwb  3918  ssopab2b  3979  soss  4017  sucssel  4102  ssorduni  4154  onnmin  4219  ssnel  4220  ssrel  4346  ssrel2  4348  ssrelrel  4358  xpss12  4363  cnvss  4426  dmss  4452  elreldm  4478  dmcosseq  4521  relssres  4566  iss  4572  resopab2  4573  issref  4625  ssrnres  4681  dfco2a  4739  cores  4742  funssres  4859  fununi  4884  funimaexglem  4899  dfimafn  5138  funimass4  5140  funimass3  5199  dff4im  5229  funfvima2  5307  funfvima3  5308  f1elima  5328  riotass2  5409  ssoprab2b  5476  resoprab2  5512  releldm2  5725  reldmtpos  5781  dmtpos  5784  rdgss  5881  iccsupr  8378  bdop  8516  bj-nnen2lp  8594
  Copyright terms: Public domain W3C validator