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

Theorem ssel 2994
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 2989 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 118 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1491 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 330 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1802 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2078 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2078 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 203 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wal 1283   = wceq 1285  wex 1422  wcel 1434  wss 2974
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987
This theorem is referenced by:  ssel2  2995  sseli  2996  sseld  2999  sstr2  3007  ssralv  3059  ssrexv  3060  ralss  3061  rexss  3062  ssconb  3106  sscon  3107  ssdif  3108  unss1  3142  ssrin  3192  difin2  3227  reuss2  3245  reupick  3249  sssnm  3548  uniss  3624  ss2iun  3695  ssiun  3722  iinss  3731  disjss2  3771  disjss1  3774  pwnss  3935  sspwb  3973  ssopab2b  4033  soss  4071  sucssel  4181  ssorduni  4233  onintonm  4263  onnmin  4313  ssnel  4314  wessep  4322  ssrel  4448  ssrel2  4450  ssrelrel  4460  xpss12  4467  cnvss  4530  dmss  4556  elreldm  4582  dmcosseq  4625  relssres  4670  iss  4678  resopab2  4679  issref  4731  ssrnres  4787  dfco2a  4845  cores  4848  funssres  4966  fununi  4992  funimaexglem  5007  dfimafn  5248  funimass4  5250  funimass3  5309  dff4im  5339  funfvima2  5417  funfvima3  5418  f1elima  5438  riotass2  5519  ssoprab2b  5587  resoprab2  5623  releldm2  5836  reldmtpos  5896  dmtpos  5899  rdgss  6026  negf1o  7542  lbreu  8079  lbinf  8082  eqreznegel  8769  negm  8770  iccsupr  9054  negfi  10237  isumrblem  10326  bdop  10809  bj-nnen2lp  10892
  Copyright terms: Public domain W3C validator