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

Theorem ssel 3557
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 3552 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 204 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2044 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 586 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1831 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2601 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2601 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 283 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1975  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549
This theorem is referenced by:  ssel2  3558  sseli  3559  sseld  3562  sstr2  3570  nelss  3622  ssrexf  3623  ssralv  3624  ssrexv  3625  ralss  3626  rexss  3627  ssconb  3700  sscon  3701  ssdif  3702  unss1  3739  ssrin  3795  difin2  3844  reuss2  3861  reupick  3865  elpwunsn  4166  sssn  4291  uniss  4384  ss2iun  4462  ssiun  4488  iinss  4497  disjss2  4546  disjss1  4549  pwnss  4747  sspwb  4834  ssopab2b  4913  pwssun  4930  soss  4963  frinxp  5093  ssrel  5116  ssrel2  5118  ssrelrel  5128  xpss12  5133  cnvssOLD  5201  dmss  5228  elreldm  5254  dmcosseq  5291  relssres  5340  iss  5350  resopab2  5351  issref  5411  ssrnres  5473  dfco2a  5534  cores  5537  oneqmini  5675  sucssel  5718  onssneli  5736  onssnel2i  5737  funssres  5826  fununi  5860  dfimafn  6136  funimass4  6138  funimass3  6222  dff3  6261  dff4  6262  funfvima2  6371  funfvima3  6373  f1elima  6395  isomin  6461  isofrlem  6464  riotass2  6511  ssoprab2b  6584  resoprab2  6629  ssorduni  6850  onint  6860  oninton  6865  ssnlim  6948  releldm2  7082  reldmtpos  7220  dmtpos  7224  wfrlem10  7284  onfununi  7298  tz7.48lem  7396  tz7.49  7400  omeulem1  7522  omeulem2  7523  omsmolem  7593  omsmo  7594  ss2ixp  7780  boxriin  7809  onomeneq  8008  unblem1  8070  unblem3  8072  fiint  8095  inf3lem2  8382  cantnflem2  8443  tcel  8477  tz9.13  8510  rankr1ag  8521  rankpwi  8542  rankelb  8543  bndrank  8560  cardlim  8654  carduni  8663  acni2  8725  dfac12r  8824  cfub  8927  cflim2  8941  fin1a2lem9  9086  axdc3lem2  9129  axdclem2  9198  gch2  9349  eltsk2g  9425  suplem1pr  9726  negn0  10306  negf1o  10307  fimaxre  10813  negfi  10816  fiminre  10817  lbreu  10818  lbinf  10821  sup2  10824  sup3  10825  infm3  10827  infregelb  10850  uzwo  11579  eqreznegel  11602  xrsupsslem  11961  xrinfmsslem  11962  supxrpnf  11972  supxrunb1  11973  supxrunb2  11974  iccsupr  12089  ssnn0fi  12597  incexclem  14349  fprodmodd  14509  sumeven  14890  sumodd  14891  gcdcllem1  15001  lcmfnnval  15117  lcmfnncl  15122  dvdslcmf  15124  lcmfunsnlem2lem2  15132  lcmfdvdsb  15136  lubel  16887  clatleglb  16891  mulgpropd  17349  sylow2a  17799  efgi2  17903  lspsnel6  18757  submabas  20141  pmatcollpw3lem  20345  elcls2  20626  isclo2  20640  cmpsublem  20950  cmpsub  20951  hauscmplem  20957  1stcelcls  21012  llyss  21030  nllyss  21031  txkgen  21203  nrmr0reg  21300  uffix  21473  ufinffr  21481  ufilen  21482  fmfnfmlem2  21507  alexsubALTlem2  21600  alexsubALT  21603  metrest  22076  iccntr  22360  reconnlem2  22366  clmneg1  22617  clmvscom  22625  caubl  22827  ulmss  23868  axcontlem4  25561  nbgranself2  25727  cusgrarn  25750  ocsh  27328  ococss  27338  shorth  27340  spansnss2  27620  h1datomi  27626  pjss2i  27725  pjssmii  27726  pjorthcoi  28214  pj3si  28252  ssrelf  28607  dfimafnf  28619  funimass4f  28620  mptssALT  28659  1stpreima  28669  2ndpreima  28670  ordtconlem1  29100  indpi1  29213  bnj518  30012  cvmlift2lem1  30340  dfon2lem6  30739  trpredmintr  30777  orderseqlem  30795  frrlem5b  30831  frrlem5d  30833  nofv  30856  nocvxminlem  30891  nocvxmin  30892  limsucncmpi  31416  finxpreclem4  32206  poimirlem3  32381  poimirlem29  32407  poimirlem32  32410  ismtyres  32576  ispridlc  32838  paddss1  33920  paddss2  33921  lspindp5  35876  pw2f1ocnv  36421  ss2iundf  36769  iunrelexp0  36812  gneispace0nelrn3  37259  nzss  37337  onfrALTlem3  37579  onfrALTlem2  37581  sspwtr  37869  sspwtrALT  37870  sspwtrALT2  37879  pwtrVD  37880  pwtrrVD  37881  suctrALT2VD  37892  suctrALT2  37893  onfrALTlem3VD  37944  onfrALTlem2VD  37946  qndenserrnopnlem  38993  dfaimafn  39695  mgmplusfreseq  41561  gsumlsscl  41956  lincfsuppcl  41994  linccl  41995
  Copyright terms: Public domain W3C validator