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

Theorem ssel 3562
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 3557 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 205 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2047 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 587 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1833 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2606 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2606 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 284 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1473   = wceq 1475  wex 1695  wcel 1977  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  ssel2  3563  sseli  3564  sseld  3567  sstr2  3575  nelss  3627  ssrexf  3628  ssralv  3629  ssrexv  3630  ralss  3631  rexss  3632  ssconb  3705  sscon  3706  ssdif  3707  unss1  3744  ssrin  3800  difin2  3849  reuss2  3866  reupick  3870  elpwunsn  4171  sssn  4298  uniss  4394  ss2iun  4472  ssiun  4498  iinss  4507  disjss2  4556  disjss1  4559  pwnss  4756  sspwb  4844  ssopab2b  4927  pwssun  4944  soss  4977  frinxp  5107  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  xpss12  5148  cnvssOLD  5217  dmss  5245  elreldm  5271  dmcosseq  5308  relssres  5357  iss  5367  resopab2  5368  issref  5428  ssrnres  5491  dfco2a  5552  cores  5555  oneqmini  5693  sucssel  5736  onssneli  5754  onssnel2i  5755  funssres  5844  fununi  5878  dfimafn  6155  funimass4  6157  funimass3  6241  dff3  6280  dff4  6281  funfvima2  6397  funfvima3  6399  f1elima  6421  isomin  6487  isofrlem  6490  riotass2  6537  ssoprab2b  6610  resoprab2  6655  ssorduni  6877  onint  6887  oninton  6892  ssnlim  6975  releldm2  7109  reldmtpos  7247  dmtpos  7251  wfrlem10  7311  onfununi  7325  tz7.48lem  7423  tz7.49  7427  omeulem1  7549  omeulem2  7550  omsmolem  7620  omsmo  7621  ss2ixp  7807  boxriin  7836  onomeneq  8035  unblem1  8097  unblem3  8099  fiint  8122  inf3lem2  8409  cantnflem2  8470  tcel  8504  tz9.13  8537  rankr1ag  8548  rankpwi  8569  rankelb  8570  bndrank  8587  cardlim  8681  carduni  8690  acni2  8752  dfac12r  8851  cfub  8954  cflim2  8968  fin1a2lem9  9113  axdc3lem2  9156  axdclem2  9225  gch2  9376  eltsk2g  9452  suplem1pr  9753  negn0  10338  negf1o  10339  fimaxre  10847  negfi  10850  fiminre  10851  lbreu  10852  lbinf  10855  sup2  10858  sup3  10859  infm3  10861  infregelb  10884  uzwo  11627  eqreznegel  11650  xrsupsslem  12009  xrinfmsslem  12010  supxrpnf  12020  supxrunb1  12021  supxrunb2  12022  iccsupr  12137  ssnn0fi  12646  incexclem  14407  fprodmodd  14567  sumeven  14948  sumodd  14949  gcdcllem1  15059  lcmfnnval  15175  lcmfnncl  15180  dvdslcmf  15182  lcmfunsnlem2lem2  15190  lcmfdvdsb  15194  lubel  16945  clatleglb  16949  mulgpropd  17407  sylow2a  17857  efgi2  17961  lspsnel6  18815  submabas  20203  pmatcollpw3lem  20407  elcls2  20688  isclo2  20702  cmpsublem  21012  cmpsub  21013  hauscmplem  21019  1stcelcls  21074  llyss  21092  nllyss  21093  txkgen  21265  nrmr0reg  21362  uffix  21535  ufinffr  21543  ufilen  21544  fmfnfmlem2  21569  alexsubALTlem2  21662  alexsubALT  21665  metrest  22139  iccntr  22432  reconnlem2  22438  clmneg1  22690  clmvscom  22698  caubl  22914  ulmss  23955  axcontlem4  25647  nbgranself2  25965  cusgrarn  25988  ocsh  27526  ococss  27536  shorth  27538  spansnss2  27818  h1datomi  27824  pjss2i  27923  pjssmii  27924  pjorthcoi  28412  pj3si  28450  ssrelf  28805  dfimafnf  28817  funimass4f  28818  mptssALT  28857  1stpreima  28867  2ndpreima  28868  ordtconlem1  29298  indpi1  29411  bnj518  30210  cvmlift2lem1  30538  dfon2lem6  30937  trpredmintr  30975  orderseqlem  30993  frrlem5b  31029  frrlem5d  31031  nofv  31054  nocvxminlem  31089  nocvxmin  31090  limsucncmpi  31614  finxpreclem4  32407  poimirlem3  32582  poimirlem29  32608  poimirlem32  32611  ismtyres  32777  ispridlc  33039  paddss1  34121  paddss2  34122  lspindp5  36077  pw2f1ocnv  36622  ss2iundf  36970  iunrelexp0  37013  gneispace0nelrn3  37460  nzss  37538  onfrALTlem3  37780  onfrALTlem2  37782  sspwtr  38070  sspwtrALT  38071  sspwtrALT2  38080  pwtrVD  38081  pwtrrVD  38082  suctrALT2VD  38093  suctrALT2  38094  onfrALTlem3VD  38145  onfrALTlem2VD  38147  qndenserrnopnlem  39193  dfaimafn  39894  mgmplusfreseq  41563  gsumlsscl  41958  lincfsuppcl  41996  linccl  41997  onsetrec  42250
  Copyright terms: Public domain W3C validator