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

Theorem ssel 3033
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 3028 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 119 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1502 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 331 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1815 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2091 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2091 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 204 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1294   = wceq 1296  wex 1433  wcel 1445  wss 3013
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026
This theorem is referenced by:  ssel2  3034  sseli  3035  sseld  3038  sstr2  3046  ssralv  3100  ssrexv  3101  ralss  3102  rexss  3103  ssconb  3148  sscon  3149  ssdif  3150  unss1  3184  ssrin  3240  difin2  3277  reuss2  3295  reupick  3299  sssnm  3620  uniss  3696  ss2iun  3767  ssiun  3794  iinss  3803  disjss2  3847  disjss1  3850  pwnss  4015  sspwb  4067  ssopab2b  4127  soss  4165  sucssel  4275  ssorduni  4332  onintonm  4362  onnmin  4412  ssnel  4413  wessep  4421  ssrel  4555  ssrel2  4557  ssrelrel  4567  xpss12  4574  cnvss  4640  dmss  4666  elreldm  4693  dmcosseq  4736  relssres  4783  iss  4791  resopab2  4792  issref  4847  ssrnres  4907  dfco2a  4965  cores  4968  funssres  5090  fununi  5116  funimaexglem  5131  dfimafn  5388  funimass4  5390  funimass3  5454  dff4im  5484  funfvima2  5566  funfvima3  5567  f1elima  5590  riotass2  5672  ssoprab2b  5744  resoprab2  5780  releldm2  5993  reldmtpos  6056  dmtpos  6059  rdgss  6186  ss2ixp  6508  fiintim  6719  negf1o  7957  lbreu  8503  lbinf  8506  eqreznegel  9198  negm  9199  iccsupr  9532  negfi  10790  sumrbdclem  10935  metrest  12308  bdop  12490  bj-nnen2lp  12573  exmidsbthrlem  12633
  Copyright terms: Public domain W3C validator