MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssel Structured version   Visualization version   GIF version

Theorem ssel 3964
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 3958 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 217 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2180 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 611 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1911 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 dfclel 2898 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 dfclel 2898 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 297 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1528   = wceq 1530  wex 1773  wcel 2107  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  ssel2  3965  sseli  3966  sseld  3969  sstr2  3977  nelss  4033  ssrexf  4034  ssralv  4036  ssrexv  4037  ralss  4040  rexss  4041  ssconb  4117  sscon  4118  ssdif  4119  unss1  4158  ssrin  4213  difin2  4269  reuss2  4286  reupick  4290  elpwunsn  4619  sssn  4757  uniss  4857  ss2iun  4933  ssiun  4966  iinss  4976  disjss2  5030  disjss1  5033  pwnss  5246  sspwb  5337  ssopab2bw  5430  ssopab2b  5432  pwssun  5453  xpss12  5568  frinxp  5632  ssrel  5655  ssrel2  5657  ssrelrel  5667  dmss  5769  elreldm  5803  dmcosseq  5842  relssres  5891  iss  5901  resopab2  5902  ssrnres  6032  dfco2a  6096  cores  6099  oneqmini  6239  sucssel  6280  onssneli  6297  onssnel2i  6298  funssres  6394  fununi  6425  dfimafn  6724  funimass4  6726  funimass3  6819  dff3  6861  dff4  6862  funfvima2  6991  funfvima3  6995  f1elima  7018  isomin  7085  isofrlem  7088  riotass2  7139  ssoprab2b  7218  eqoprab2bw  7219  resoprab2  7264  ssorduni  7491  onint  7501  oninton  7506  ssnlim  7590  releldm2  7736  dmtpos  7898  wfrlem10  7958  onfununi  7972  tz7.48lem  8071  tz7.49  8075  omeulem1  8201  omeulem2  8202  omsmolem  8273  omsmo  8274  ss2ixp  8466  boxriin  8496  onomeneq  8700  unblem1  8762  unblem3  8764  fiint  8787  inf3lem2  9084  cantnflem2  9145  tcel  9179  tz9.13  9212  rankr1ag  9223  rankpwi  9244  rankelb  9245  bndrank  9262  cardlim  9393  carduni  9402  acni2  9464  dfac12r  9564  cfub  9663  cflim2  9677  fin1a2lem9  9822  axdc3lem2  9865  axdclem2  9934  gch2  10089  eltsk2g  10165  suplem1pr  10466  negn0  11061  negf1o  11062  fimaxreOLD  11577  negfi  11581  fiminreOLD  11582  lbreu  11583  lbinf  11586  sup2  11589  sup3  11590  infm3  11592  infregelb  11617  uzwo  12303  eqreznegel  12326  xrsupsslem  12693  xrinfmsslem  12694  supxrpnf  12704  supxrunb1  12705  supxrunb2  12706  iccsupr  12823  ssnn0fi  13346  incexclem  15183  fprodmodd  15343  sumeven  15730  sumodd  15731  gcdcllem1  15840  lcmfnnval  15960  lcmfnncl  15965  dvdslcmf  15967  lcmfunsnlem2lem2  15975  lcmfdvdsb  15979  lubel  17724  clatleglb  17728  mulgpropd  18201  sylow2a  18666  efgi2  18773  lspsnel6  19688  submabas  21103  pmatcollpw3lem  21307  elcls2  21598  isclo2  21612  cmpsublem  21923  cmpsub  21924  hauscmplem  21930  1stcelcls  21985  llyss  22003  nllyss  22004  txkgen  22176  nrmr0reg  22273  uffix  22445  ufinffr  22453  ufilen  22454  fmfnfmlem2  22479  alexsubALTlem2  22572  alexsubALT  22575  metrest  23049  iccntr  23344  reconnlem2  23350  clmneg1  23601  clmvscom  23609  caubl  23826  ulmss  24900  axcontlem4  26667  ocsh  28974  ococss  28984  shorth  28986  spansnss2  29266  h1datomi  29272  pjss2i  29371  pjssmii  29372  pjorthcoi  29860  pj3si  29898  ssrelf  30281  dfimafnf  30296  funimass4f  30297  mptssALT  30335  1stpreima  30355  2ndpreima  30356  isprmidlc  30868  ordtconnlem1  31053  indpi1  31165  bnj518  32044  cvmlift2lem1  32433  satffunlem2lem1  32535  satfvel  32543  dfon2lem6  32917  trpredmintr  32954  orderseqlem  32978  nofv  33048  nocvxminlem  33131  nocvxmin  33132  limsucncmpi  33677  finxpreclem4  34544  poimirlem3  34762  poimirlem29  34788  poimirlem32  34791  ismtyres  34954  ispridlc  35216  iss2  35469  paddss1  36820  paddss2  36821  lspindp5  38773  dffltz  39132  pw2f1ocnv  39495  ss2iundf  39865  iunrelexp0  39908  gneispace0nelrn3  40353  nzss  40510  onfrALTlem3  40739  onfrALTlem2  40741  sspwtr  41016  sspwtrALT  41017  sspwtrALT2  41018  pwtrVD  41019  pwtrrVD  41020  suctrALT2VD  41031  suctrALT2  41032  onfrALTlem3VD  41082  onfrALTlem2VD  41084  iinssf  41268  qndenserrnopnlem  42444  dfaimafn  43226  sprsymrelfolem2  43483  mgmplusfreseq  43868  gsumlsscl  44259  lincfsuppcl  44296  linccl  44297  onsetrec  44638
  Copyright terms: Public domain W3C validator