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

Theorem ssel 3589
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 3584 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 206 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2057 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 588 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1844 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2616 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2616 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 285 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1479   = wceq 1481  wex 1702  wcel 1988  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  ssel2  3590  sseli  3591  sseld  3594  sstr2  3602  nelss  3656  ssrexf  3657  ssralv  3658  ssrexv  3659  ralss  3660  rexss  3661  ssconb  3735  sscon  3736  ssdif  3737  unss1  3774  ssrin  3830  difin2  3882  reuss2  3899  reupick  3903  elpwunsn  4215  sssn  4349  uniss  4449  ss2iun  4527  ssiun  4553  iinss  4562  disjss2  4614  disjss1  4617  pwnss  4821  sspwb  4908  ssopab2b  4992  pwssun  5010  soss  5043  frinxp  5174  ssrel  5197  ssrelOLD  5198  ssrel2  5200  ssrelrel  5210  xpss12  5215  cnvssOLD  5284  dmss  5312  elreldm  5339  dmcosseq  5376  relssres  5425  iss  5435  resopab2  5436  issref  5497  ssrnres  5560  dfco2a  5623  cores  5626  oneqmini  5764  sucssel  5807  onssneli  5825  onssnel2i  5826  funssres  5918  fununi  5952  dfimafn  6232  funimass4  6234  funimass3  6319  dff3  6358  dff4  6359  funfvima2  6478  funfvima3  6480  f1elima  6505  isomin  6572  isofrlem  6575  riotass2  6623  ssoprab2b  6697  resoprab2  6742  ssorduni  6970  onint  6980  oninton  6985  ssnlim  7068  releldm2  7203  reldmtpos  7345  dmtpos  7349  wfrlem10  7409  onfununi  7423  tz7.48lem  7521  tz7.49  7525  omeulem1  7647  omeulem2  7648  omsmolem  7718  omsmo  7719  ss2ixp  7906  boxriin  7935  onomeneq  8135  unblem1  8197  unblem3  8199  fiint  8222  inf3lem2  8511  cantnflem2  8572  tcel  8606  tz9.13  8639  rankr1ag  8650  rankpwi  8671  rankelb  8672  bndrank  8689  cardlim  8783  carduni  8792  acni2  8854  dfac12r  8953  cfub  9056  cflim2  9070  fin1a2lem9  9215  axdc3lem2  9258  axdclem2  9327  gch2  9482  eltsk2g  9558  suplem1pr  9859  negn0  10444  negf1o  10445  fimaxre  10953  negfi  10956  fiminre  10957  lbreu  10958  lbinf  10961  sup2  10964  sup3  10965  infm3  10967  infregelb  10992  uzwo  11736  eqreznegel  11759  xrsupsslem  12122  xrinfmsslem  12123  supxrpnf  12133  supxrunb1  12134  supxrunb2  12135  iccsupr  12251  ssnn0fi  12767  incexclem  14549  fprodmodd  14709  sumeven  15091  sumodd  15092  gcdcllem1  15202  lcmfnnval  15318  lcmfnncl  15323  dvdslcmf  15325  lcmfunsnlem2lem2  15333  lcmfdvdsb  15337  lubel  17103  clatleglb  17107  mulgpropd  17565  sylow2a  18015  efgi2  18119  lspsnel6  18975  submabas  20365  pmatcollpw3lem  20569  elcls2  20859  isclo2  20873  cmpsublem  21183  cmpsub  21184  hauscmplem  21190  1stcelcls  21245  llyss  21263  nllyss  21264  txkgen  21436  nrmr0reg  21533  uffix  21706  ufinffr  21714  ufilen  21715  fmfnfmlem2  21740  alexsubALTlem2  21833  alexsubALT  21836  metrest  22310  iccntr  22605  reconnlem2  22611  clmneg1  22863  clmvscom  22871  caubl  23087  ulmss  24132  axcontlem4  25828  ocsh  28112  ococss  28122  shorth  28124  spansnss2  28404  h1datomi  28410  pjss2i  28509  pjssmii  28510  pjorthcoi  28998  pj3si  29036  ssrelf  29397  dfimafnf  29409  funimass4f  29410  mptssALT  29448  1stpreima  29458  2ndpreima  29459  ordtconnlem1  29944  indpi1  30056  bnj518  30930  cvmlift2lem1  31258  dfon2lem6  31667  trpredmintr  31705  orderseqlem  31723  frrlem5b  31759  frrlem5d  31761  nofv  31784  nocvxminlem  31867  nocvxmin  31868  limsucncmpi  32419  finxpreclem4  33202  poimirlem3  33383  poimirlem29  33409  poimirlem32  33412  ismtyres  33578  ispridlc  33840  paddss1  34922  paddss2  34923  lspindp5  36878  pw2f1ocnv  37423  ss2iundf  37770  iunrelexp0  37813  gneispace0nelrn3  38260  nzss  38336  onfrALTlem3  38579  onfrALTlem2  38581  sspwtr  38868  sspwtrALT  38869  sspwtrALT2  38878  pwtrVD  38879  pwtrrVD  38880  suctrALT2VD  38891  suctrALT2  38892  onfrALTlem3VD  38943  onfrALTlem2VD  38945  iinssf  39147  qndenserrnopnlem  40280  dfaimafn  41008  sprsymrelfolem2  41508  mgmplusfreseq  41538  gsumlsscl  41929  lincfsuppcl  41967  linccl  41968  onsetrec  42216
  Copyright terms: Public domain W3C validator