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

Theorem ssel 3151
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 3146 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 120 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1558 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 337 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1880 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2173 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2173 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 205 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wal 1351   = wceq 1353  wex 1492  wcel 2148  wss 3131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144
This theorem is referenced by:  ssel2  3152  sseli  3153  sseld  3156  sstr2  3164  nelss  3218  ssrexf  3219  ssralv  3221  ssrexv  3222  ralss  3223  rexss  3224  ssconb  3270  sscon  3271  ssdif  3272  unss1  3306  ssrin  3362  difin2  3399  reuss2  3417  reupick  3421  sssnm  3756  uniss  3832  ss2iun  3903  ssiun  3930  iinss  3940  disjss2  3985  disjss1  3988  pwnss  4161  sspwb  4218  ssopab2b  4278  soss  4316  sucssel  4426  ssorduni  4488  onintonm  4518  onnmin  4569  ssnel  4570  wessep  4579  ssrel  4716  ssrel2  4718  ssrelrel  4728  xpss12  4735  cnvss  4802  dmss  4828  elreldm  4855  dmcosseq  4900  relssres  4947  iss  4955  resopab2  4956  issref  5013  ssrnres  5073  dfco2a  5131  cores  5134  funssres  5260  fununi  5286  funimaexglem  5301  dfimafn  5566  funimass4  5568  funimass3  5634  dff4im  5664  funfvima2  5751  funfvima3  5752  f1elima  5776  riotass2  5859  ssoprab2b  5934  resoprab2  5974  releldm2  6188  reldmtpos  6256  dmtpos  6259  rdgss  6386  ss2ixp  6713  fiintim  6930  negf1o  8341  lbreu  8904  lbinf  8907  eqreznegel  9616  negm  9617  iccsupr  9968  negfi  11238  sumrbdclem  11387  prodrbdclem  11581  fprodmodd  11651  mulgpropdg  13030  subgintm  13063  subrgintm  13369  lspsnel6  13499  metrest  14091  bdop  14712  bj-nnen2lp  14791  exmidsbthrlem  14855
  Copyright terms: Public domain W3C validator