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

Theorem ssel 2964
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 2959 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 117 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1464 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 324 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1774 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2050 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2050 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 198 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wal 1255   = wceq 1257  wex 1395  wcel 1407  wss 2942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-11 1411  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-in 2949  df-ss 2956
This theorem is referenced by:  ssel2  2965  sseli  2966  sseld  2969  sstr2  2977  ssralv  3029  ssrexv  3030  ralss  3031  rexss  3032  ssconb  3101  sscon  3102  ssdif  3103  unss1  3137  ssrin  3187  difin2  3224  reuss2  3242  reupick  3246  sssnm  3550  uniss  3626  ss2iun  3697  ssiun  3724  iinss  3733  disjss2  3773  disjss1  3776  pwnss  3937  sspwb  3977  ssopab2b  4038  soss  4076  sucssel  4186  ssorduni  4238  onintonm  4268  onnmin  4317  ssnel  4318  wessep  4327  ssrel  4453  ssrel2  4455  ssrelrel  4465  xpss12  4470  cnvss  4533  dmss  4559  elreldm  4585  dmcosseq  4628  relssres  4673  iss  4679  resopab2  4680  issref  4732  ssrnres  4788  dfco2a  4846  cores  4849  funssres  4967  fununi  4992  funimaexglem  5007  dfimafn  5247  funimass4  5249  funimass3  5308  dff4im  5338  funfvima2  5416  funfvima3  5417  f1elima  5437  riotass2  5519  ssoprab2b  5587  resoprab2  5623  releldm2  5836  reldmtpos  5896  dmtpos  5899  rdgss  5998  eqreznegel  8616  negm  8617  iccsupr  8906  bdop  10325  bj-nnen2lp  10409
  Copyright terms: Public domain W3C validator