Theorem ssel 3915

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2185. (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		df-ss 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 613	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2812	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2812	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906

This theorem is referenced by:  ssel2  3916  sseli  3917  sseld  3920  sstr2OLD  3929  nelss  3987  ssrexf  3988  ssralvOLD  3994  ssrexvOLD  3995  ralssOLD  3998  rexssOLD  3999  rabss2  4017  ssconb  4082  sscon  4083  ssdif  4084  unss1  4125  ssrin  4182  difin2  4241  reuss2  4266  reupick  4269  elpwunsn  4628  sssn  4769  uniss  4858  ss2iun  4952  ssiun  4989  iinss  4999  disjss2  5055  disjss1  5058  pwnss  5293  sspwb  5401  ssopab2bw  5502  ssopab2b  5504  pwssun  5523  xpss12  5646  frinxp  5714  ssrel  5739  ssrel2  5741  ssrelrel  5752  dmss  5857  elreldm  5890  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  relssres  5987  iss  6000  resopab2  6001  imadifssran  6115  ssrnres  6142  dfco2a  6210  cores  6213  oneqmini  6376  sucssel  6420  onssneli  6440  onssnel2i  6441  funssres  6542  fununi  6573  dfimafn  6902  funimass4  6904  funimass3  7006  dff3  7052  dff4  7053  funfvima2  7186  funfvima3  7191  f1elima  7218  isomin  7292  isofrlem  7295  riotass2  7354  ssoprab2b  7436  eqoprab2bw  7437  resoprab2  7486  ssorduni  7733  onint  7744  oninton  7749  ssnlim  7837  mptcnfimad  7939  releldm2  7996  orderseqlem  8107  dmtpos  8188  onfununi  8281  tz7.48lem  8380  tz7.49  8384  omeulem1  8517  omeulem2  8518  omsmolem  8593  omsmo  8594  ss2ixp  8858  boxriin  8888  unblem1  9202  unblem3  9204  fiint  9237  inf3lem2  9550  cantnflem2  9611  tcel  9664  tz9.13  9715  rankr1ag  9726  rankpwi  9747  rankelb  9748  bndrank  9765  cardlim  9896  carduni  9905  acni2  9968  dfac12r  10069  cfub  10171  cflim2  10185  fin1a2lem9  10330  axdc3lem2  10373  axdclem2  10442  gch2  10598  eltsk2g  10674  suplem1pr  10975  negn0  11579  negf1o  11580  negfi  12105  lbreu  12106  lbinf  12109  sup2  12112  sup3  12113  infm3  12115  infregelb  12140  indpi1  12173  uzwo  12861  eqreznegel  12884  xrsupsslem  13259  xrinfmsslem  13260  supxrpnf  13270  supxrunb1  13271  supxrunb2  13272  iccsupr  13395  ssnn0fi  13947  incexclem  15801  fprodmodd  15962  sumeven  16356  sumodd  16357  gcdcllem1  16468  lcmfnnval  16593  lcmfnncl  16598  dvdslcmf  16600  lcmfunsnlem2lem2  16608  lcmfdvdsb  16612  lubel  18480  clatleglb  18484  smndex1mgm  18878  smndex1sgrp  18879  smndex1mnd  18881  mulgpropd  19092  sylow2a  19594  efgi2  19700  ellspsn6  20989  rnglidlmcl  21214  submabas  22543  pmatcollpw3lem  22748  elcls2  23039  isclo2  23053  cmpsublem  23364  cmpsub  23365  hauscmplem  23371  1stcelcls  23426  llyss  23444  nllyss  23445  txkgen  23617  nrmr0reg  23714  uffix  23886  ufinffr  23894  ufilen  23895  fmfnfmlem2  23920  alexsubALTlem2  24013  alexsubALT  24016  metrest  24489  iccntr  24787  reconnlem2  24793  clmneg1  25049  clmvscom  25057  caubl  25275  dvply2g  26251  ulmss  26362  nofv  27621  nocvxminlem  27746  nocvxmin  27747  axcontlem4  29036  ocsh  31354  ococss  31364  shorth  31366  spansnss2  31646  h1datomi  31652  pjss2i  31751  pjssmii  31752  pjorthcoi  32240  pj3si  32278  ssrelf  32688  dfimafnf  32709  funimass4f  32710  mptssALT  32747  1stpreima  32780  2ndpreima  32781  isprmidlc  33507  ordtconnlem1  34068  bnj518  35028  fissorduni  35233  nummin  35236  tz9.1regs  35278  cvmlift2lem1  35484  satffunlem2lem1  35586  satfvel  35594  dfon2lem6  35968  limsucncmpi  36627  finxpreclem4  37710  poimirlem3  37944  poimirlem29  37970  poimirlem32  37973  ismtyres  38129  ispridlc  38391  iss2  38665  paddss1  40263  paddss2  40264  lspindp5  42216  sn-sup2  42936  sn-sup3d  42937  dffltz  43067  pw2f1ocnv  43465  onsupmaxb  43667  naddwordnexlem2  43826  ss2iundf  44086  iunrelexp0  44129  gneispace0nelrn3  44569  nzss  44744  onfrALTlem3  44971  onfrALTlem2  44973  sspwtr  45247  sspwtrALT  45248  sspwtrALT2  45249  pwtrVD  45250  pwtrrVD  45251  suctrALT2VD  45262  suctrALT2  45263  onfrALTlem3VD  45313  onfrALTlem2VD  45315  relpmin  45379  relpfrlem  45380  ssclaxsep  45409  omssaxinf2  45415  iinssf  45568  qndenserrnopnlem  46725  dfaimafn  47613  sprsymrelfolem2  47953  mgmplusfreseq  48641  gsumlsscl  48856  lincfsuppcl  48889  linccl  48890  onsetrec  50183