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

Theorem ssel 3630
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 3624 . . . . . 6 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 206 . . . . 5 (𝐴𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 2097 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
43anim2d 588 . . 3 (𝐴𝐵 → ((𝑥 = 𝐶𝑥𝐴) → (𝑥 = 𝐶𝑥𝐵)))
54eximdv 1886 . 2 (𝐴𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) → ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2647 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2647 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73imtr4g 285 1 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  ssel2  3631  sseli  3632  sseld  3635  sstr2  3643  nelss  3697  ssrexf  3698  ssralv  3699  ssrexv  3700  ralss  3701  rexss  3702  ssconb  3776  sscon  3777  ssdif  3778  unss1  3815  ssrin  3871  difin2  3923  reuss2  3940  reupick  3944  elpwunsn  4256  sssn  4390  uniss  4490  ss2iun  4568  ssiun  4594  iinss  4603  disjss2  4655  disjss1  4658  pwnss  4860  sspwb  4947  ssopab2b  5031  pwssun  5049  soss  5082  xpss12  5158  frinxp  5218  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  dmss  5355  elreldm  5382  dmcosseq  5419  relssres  5472  iss  5482  resopab2  5483  issref  5544  ssrnres  5607  dfco2a  5673  cores  5676  oneqmini  5814  sucssel  5857  onssneli  5875  onssnel2i  5876  funssres  5968  fununi  6002  dfimafn  6284  funimass4  6286  funimass3  6373  dff3  6412  dff4  6413  funfvima2  6533  funfvima3  6535  f1elima  6560  isomin  6627  isofrlem  6630  riotass2  6678  ssoprab2b  6754  resoprab2  6799  ssorduni  7027  onint  7037  oninton  7042  ssnlim  7125  releldm2  7262  reldmtpos  7405  dmtpos  7409  wfrlem10  7469  onfununi  7483  tz7.48lem  7581  tz7.49  7585  omeulem1  7707  omeulem2  7708  omsmolem  7778  omsmo  7779  ss2ixp  7963  boxriin  7992  onomeneq  8191  unblem1  8253  unblem3  8255  fiint  8278  inf3lem2  8564  cantnflem2  8625  tcel  8659  tz9.13  8692  rankr1ag  8703  rankpwi  8724  rankelb  8725  bndrank  8742  cardlim  8836  carduni  8845  acni2  8907  dfac12r  9006  cfub  9109  cflim2  9123  fin1a2lem9  9268  axdc3lem2  9311  axdclem2  9380  gch2  9535  eltsk2g  9611  suplem1pr  9912  negn0  10497  negf1o  10498  fimaxre  11006  negfi  11009  fiminre  11010  lbreu  11011  lbinf  11014  sup2  11017  sup3  11018  infm3  11020  infregelb  11045  uzwo  11789  eqreznegel  11812  xrsupsslem  12175  xrinfmsslem  12176  supxrpnf  12186  supxrunb1  12187  supxrunb2  12188  iccsupr  12304  ssnn0fi  12824  incexclem  14612  fprodmodd  14772  sumeven  15157  sumodd  15158  gcdcllem1  15268  lcmfnnval  15384  lcmfnncl  15389  dvdslcmf  15391  lcmfunsnlem2lem2  15399  lcmfdvdsb  15403  lubel  17169  clatleglb  17173  mulgpropd  17631  sylow2a  18080  efgi2  18184  lspsnel6  19042  submabas  20432  pmatcollpw3lem  20636  elcls2  20926  isclo2  20940  cmpsublem  21250  cmpsub  21251  hauscmplem  21257  1stcelcls  21312  llyss  21330  nllyss  21331  txkgen  21503  nrmr0reg  21600  uffix  21772  ufinffr  21780  ufilen  21781  fmfnfmlem2  21806  alexsubALTlem2  21899  alexsubALT  21902  metrest  22376  iccntr  22671  reconnlem2  22677  clmneg1  22928  clmvscom  22936  caubl  23152  ulmss  24196  axcontlem4  25892  ocsh  28270  ococss  28280  shorth  28282  spansnss2  28562  h1datomi  28568  pjss2i  28667  pjssmii  28668  pjorthcoi  29156  pj3si  29194  ssrelf  29553  dfimafnf  29564  funimass4f  29565  mptssALT  29602  1stpreima  29612  2ndpreima  29613  ordtconnlem1  30098  indpi1  30210  bnj518  31082  cvmlift2lem1  31410  dfon2lem6  31817  trpredmintr  31855  orderseqlem  31877  frrlem5b  31910  frrlem5d  31912  nofv  31935  nocvxminlem  32018  nocvxmin  32019  limsucncmpi  32569  finxpreclem4  33361  poimirlem3  33542  poimirlem29  33568  poimirlem32  33571  ismtyres  33737  ispridlc  33999  iss2  34252  paddss1  35421  paddss2  35422  lspindp5  37376  pw2f1ocnv  37921  ss2iundf  38268  iunrelexp0  38311  gneispace0nelrn3  38757  nzss  38833  onfrALTlem3  39076  onfrALTlem2  39078  sspwtr  39365  sspwtrALT  39366  sspwtrALT2  39372  pwtrVD  39373  pwtrrVD  39374  suctrALT2VD  39385  suctrALT2  39386  onfrALTlem3VD  39437  onfrALTlem2VD  39439  iinssf  39641  qndenserrnopnlem  40835  dfaimafn  41566  sprsymrelfolem2  42068  mgmplusfreseq  42098  gsumlsscl  42489  lincfsuppcl  42527  linccl  42528  onsetrec  42779
  Copyright terms: Public domain W3C validator