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

Theorem ssel 2916
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 2911 . . . . . 6 (ABx(x Ax B))
21biimpi 113 . . . . 5 (ABx(x Ax B))
3219.21bi 1432 . . . 4 (AB → (x Ax B))
43anim2d 320 . . 3 (AB → ((x = 𝐶 x A) → (x = 𝐶 x B)))
54eximdv 1742 . 2 (AB → (x(x = 𝐶 x A) → x(x = 𝐶 x B)))
6 df-clel 2018 . 2 (𝐶 Ax(x = 𝐶 x A))
7 df-clel 2018 . 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 1226   = wceq 1228  wex 1362   wcel 1374  wss 2894
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 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908
This theorem is referenced by:  ssel2  2917  sseli  2918  sseld  2921  sstr2  2929  ssralv  2981  ssrexv  2982  ralss  2983  rexss  2984  ssconb  3053  sscon  3054  ssdif  3055  unss1  3089  ssrin  3139  difin2  3176  reuss2  3194  reupick  3198  sssnm  3499  uniss  3575  ss2iun  3646  ssiun  3673  iinss  3682  disjss2  3722  disjss1  3725  pwnss  3886  sspwb  3926  ssopab2b  3987  soss  4025  sucssel  4111  ssorduni  4163  onnmin  4228  ssnel  4229  ssrel  4355  ssrel2  4357  ssrelrel  4367  xpss12  4372  cnvss  4435  dmss  4461  elreldm  4487  dmcosseq  4530  relssres  4575  iss  4581  resopab2  4582  issref  4634  ssrnres  4690  dfco2a  4748  cores  4751  funssres  4868  fununi  4893  funimaexglem  4908  dfimafn  5147  funimass4  5149  funimass3  5208  dff4im  5238  funfvima2  5316  funfvima3  5317  f1elima  5337  riotass2  5418  ssoprab2b  5485  resoprab2  5521  releldm2  5734  reldmtpos  5790  dmtpos  5793  rdgss  5890  bdop  7249  bj-nnen2lp  7323
  Copyright terms: Public domain W3C validator