Theorem ssel 3915

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2172. (Revised by SN, 27-May-2024.)

Assertion

Ref	Expression
ssel	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem ssel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3908	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 612	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1835	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2818	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2818	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 216	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  ssel2  3917  sseli  3918  sseld  3921  sstr2  3929  nelss  3985  ssrexf  3986  ssralv  3988  ssrexv  3989  ralss  3992  rexss  3993  ssconb  4073  sscon  4074  ssdif  4075  unss1  4114  ssrin  4168  difin2  4226  reuss2  4250  reupick  4253  elpwunsn  4620  sssn  4760  uniss  4848  ss2iun  4943  ssiun  4977  iinss  4987  disjss2  5043  disjss1  5046  pwnss  5273  sspwb  5366  ssopab2bw  5461  ssopab2b  5463  pwssun  5486  xpss12  5605  frinxp  5670  ssrel  5694  ssrelOLD  5695  ssrel2  5697  ssrelrel  5708  dmss  5814  elreldm  5847  dmcosseq  5885  relssres  5935  iss  5946  resopab2  5947  ssrnres  6086  dfco2a  6154  cores  6157  oneqmini  6321  sucssel  6362  onssneli  6380  onssnel2i  6381  funssres  6485  fununi  6516  dfimafn  6841  funimass4  6843  funimass3  6940  dff3  6985  dff4  6986  funfvima2  7116  funfvima3  7121  f1elima  7145  isomin  7217  isofrlem  7220  riotass2  7272  ssoprab2b  7353  eqoprab2bw  7354  resoprab2  7402  ssorduni  7638  onint  7649  oninton  7654  ssnlim  7741  releldm2  7893  dmtpos  8063  wfrlem10OLD  8158  onfununi  8181  tz7.48lem  8281  tz7.49  8285  omeulem1  8422  omeulem2  8423  omsmolem  8496  omsmo  8497  ss2ixp  8707  boxriin  8737  onomeneqOLD  9021  unblem1  9075  unblem3  9077  fiint  9100  inf3lem2  9396  cantnflem2  9457  tcel  9512  tz9.13  9558  rankr1ag  9569  rankpwi  9590  rankelb  9591  bndrank  9608  cardlim  9739  carduni  9748  acni2  9811  dfac12r  9911  cfub  10014  cflim2  10028  fin1a2lem9  10173  axdc3lem2  10216  axdclem2  10285  gch2  10440  eltsk2g  10516  suplem1pr  10817  negn0  11413  negf1o  11414  negfi  11933  lbreu  11934  lbinf  11937  sup2  11940  sup3  11941  infm3  11943  infregelb  11968  uzwo  12660  eqreznegel  12683  xrsupsslem  13050  xrinfmsslem  13051  supxrpnf  13061  supxrunb1  13062  supxrunb2  13063  iccsupr  13183  ssnn0fi  13714  incexclem  15557  fprodmodd  15716  sumeven  16105  sumodd  16106  gcdcllem1  16215  lcmfnnval  16338  lcmfnncl  16343  dvdslcmf  16345  lcmfunsnlem2lem2  16353  lcmfdvdsb  16357  lubel  18241  clatleglb  18245  smndex1mgm  18555  smndex1sgrp  18556  smndex1mnd  18558  mulgpropd  18754  sylow2a  19233  efgi2  19340  lspsnel6  20265  submabas  21736  pmatcollpw3lem  21941  elcls2  22234  isclo2  22248  cmpsublem  22559  cmpsub  22560  hauscmplem  22566  1stcelcls  22621  llyss  22639  nllyss  22640  txkgen  22812  nrmr0reg  22909  uffix  23081  ufinffr  23089  ufilen  23090  fmfnfmlem2  23115  alexsubALTlem2  23208  alexsubALT  23211  metrest  23689  iccntr  23993  reconnlem2  23999  clmneg1  24254  clmvscom  24262  caubl  24481  ulmss  25565  axcontlem4  27344  ocsh  29654  ococss  29664  shorth  29666  spansnss2  29946  h1datomi  29952  pjss2i  30051  pjssmii  30052  pjorthcoi  30540  pj3si  30578  ssrelf  30964  dfimafnf  30980  funimass4f  30981  mptssALT  31021  1stpreima  31048  2ndpreima  31049  isprmidlc  31632  ordtconnlem1  31883  indpi1  31997  bnj518  32875  nummin  33072  cvmlift2lem1  33273  satffunlem2lem1  33375  satfvel  33383  dfon2lem6  33773  orderseqlem  33810  nofv  33869  nocvxminlem  33981  nocvxmin  33982  limsucncmpi  34643  finxpreclem4  35574  poimirlem3  35789  poimirlem29  35815  poimirlem32  35818  ismtyres  35975  ispridlc  36237  iss2  36486  paddss1  37838  paddss2  37839  lspindp5  39791  sn-sup2  40446  dffltz  40478  pw2f1ocnv  40866  ss2iundf  41274  iunrelexp0  41317  gneispace0nelrn3  41759  nzss  41942  onfrALTlem3  42171  onfrALTlem2  42173  sspwtr  42448  sspwtrALT  42449  sspwtrALT2  42450  pwtrVD  42451  pwtrrVD  42452  suctrALT2VD  42463  suctrALT2  42464  onfrALTlem3VD  42514  onfrALTlem2VD  42516  iinssf  42694  qndenserrnopnlem  43845  dfaimafn  44668  sprsymrelfolem2  44956  mgmplusfreseq  45338  gsumlsscl  45730  lincfsuppcl  45765  linccl  45766  onsetrec  46424