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

Theorem ssel 3008
Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssel (𝐴𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem ssel
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfss2 3003 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 118 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1493 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 330 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1805 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2081 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2081 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 203 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wal 1285   = wceq 1287  wex 1424  wcel 1436  wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001
This theorem is referenced by:  ssel2  3009  sseli  3010  sseld  3013  sstr2  3021  ssralv  3074  ssrexv  3075  ralss  3076  rexss  3077  ssconb  3122  sscon  3123  ssdif  3124  unss1  3158  ssrin  3214  difin2  3250  reuss2  3268  reupick  3272  sssnm  3581  uniss  3657  ss2iun  3728  ssiun  3755  iinss  3764  disjss2  3804  disjss1  3807  pwnss  3969  sspwb  4017  ssopab2b  4077  soss  4115  sucssel  4225  ssorduni  4277  onintonm  4307  onnmin  4357  ssnel  4358  wessep  4366  ssrel  4494  ssrel2  4496  ssrelrel  4506  xpss12  4513  cnvss  4577  dmss  4603  elreldm  4629  dmcosseq  4672  relssres  4717  iss  4725  resopab2  4726  issref  4781  ssrnres  4839  dfco2a  4897  cores  4900  funssres  5021  fununi  5047  funimaexglem  5062  dfimafn  5316  funimass4  5318  funimass3  5378  dff4im  5408  funfvima2  5488  funfvima3  5489  f1elima  5513  riotass2  5595  ssoprab2b  5663  resoprab2  5699  releldm2  5912  reldmtpos  5972  dmtpos  5975  rdgss  6102  negf1o  7804  lbreu  8341  lbinf  8344  eqreznegel  9031  negm  9032  iccsupr  9316  negfi  10552  isumrblem  10655  bdop  11204  bj-nnen2lp  11287  exmidsbthrlem  11350
  Copyright terms: Public domain W3C validator