Theorem ssel 3937

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3928

This theorem is referenced by:  ssel2  3938  sseli  3939  sseld  3942  sstr2OLD  3951  nelss  4009  ssrexf  4010  ssralvOLD  4016  ssrexvOLD  4017  ralssOLD  4020  rexssOLD  4021  ssconb  4101  sscon  4102  ssdif  4103  unss1  4144  ssrin  4201  difin2  4260  reuss2  4285  reupick  4288  elpwunsn  4644  sssn  4786  uniss  4875  ss2iun  4970  ssiun  5005  iinss  5015  disjss2  5072  disjss1  5075  pwnss  5302  sspwb  5404  ssopab2bw  5502  ssopab2b  5504  pwssun  5523  xpss12  5646  frinxp  5714  ssrel  5737  ssrel2  5739  ssrelrel  5750  dmss  5856  elreldm  5888  dmcosseq  5929  dmcosseqOLD  5930  relssres  5982  iss  5995  resopab2  5996  imadifssran  6112  ssrnres  6139  dfco2a  6207  cores  6210  oneqmini  6373  sucssel  6417  onssneli  6438  onssnel2i  6439  funssres  6544  fununi  6575  dfimafn  6905  funimass4  6907  funimass3  7008  dff3  7054  dff4  7055  funfvima2  7187  funfvima3  7192  f1elima  7220  isomin  7294  isofrlem  7297  riotass2  7356  ssoprab2b  7438  eqoprab2bw  7439  resoprab2  7488  ssorduni  7735  onint  7746  oninton  7751  ssnlim  7842  mptcnfimad  7944  releldm2  8001  orderseqlem  8113  dmtpos  8194  onfununi  8287  tz7.48lem  8386  tz7.49  8390  omeulem1  8523  omeulem2  8524  omsmolem  8598  omsmo  8599  ss2ixp  8860  boxriin  8890  unblem1  9215  unblem3  9217  fiint  9253  fiintOLD  9254  inf3lem2  9558  cantnflem2  9619  tcel  9674  tz9.13  9720  rankr1ag  9731  rankpwi  9752  rankelb  9753  bndrank  9770  cardlim  9901  carduni  9910  acni2  9975  dfac12r  10076  cfub  10178  cflim2  10192  fin1a2lem9  10337  axdc3lem2  10380  axdclem2  10449  gch2  10604  eltsk2g  10680  suplem1pr  10981  negn0  11583  negf1o  11584  negfi  12108  lbreu  12109  lbinf  12112  sup2  12115  sup3  12116  infm3  12118  infregelb  12143  uzwo  12846  eqreznegel  12869  xrsupsslem  13243  xrinfmsslem  13244  supxrpnf  13254  supxrunb1  13255  supxrunb2  13256  iccsupr  13379  ssnn0fi  13926  incexclem  15778  fprodmodd  15939  sumeven  16333  sumodd  16334  gcdcllem1  16445  lcmfnnval  16570  lcmfnncl  16575  dvdslcmf  16577  lcmfunsnlem2lem2  16585  lcmfdvdsb  16589  lubel  18455  clatleglb  18459  smndex1mgm  18816  smndex1sgrp  18817  smndex1mnd  18819  mulgpropd  19030  sylow2a  19533  efgi2  19639  ellspsn6  20932  rnglidlmcl  21158  submabas  22498  pmatcollpw3lem  22703  elcls2  22994  isclo2  23008  cmpsublem  23319  cmpsub  23320  hauscmplem  23326  1stcelcls  23381  llyss  23399  nllyss  23400  txkgen  23572  nrmr0reg  23669  uffix  23841  ufinffr  23849  ufilen  23850  fmfnfmlem2  23875  alexsubALTlem2  23968  alexsubALT  23971  metrest  24445  iccntr  24743  reconnlem2  24749  clmneg1  25015  clmvscom  25023  caubl  25241  dvply2g  26225  ulmss  26339  nofv  27602  nocvxminlem  27723  nocvxmin  27724  axcontlem4  28947  ocsh  31262  ococss  31272  shorth  31274  spansnss2  31554  h1datomi  31560  pjss2i  31659  pjssmii  31660  pjorthcoi  32148  pj3si  32186  ssrelf  32593  dfimafnf  32610  funimass4f  32611  mptssALT  32649  1stpreima  32680  2ndpreima  32681  indpi1  32833  isprmidlc  33411  ordtconnlem1  33907  bnj518  34869  nummin  35074  cvmlift2lem1  35282  satffunlem2lem1  35384  satfvel  35392  dfon2lem6  35769  limsucncmpi  36426  finxpreclem4  37375  poimirlem3  37610  poimirlem29  37636  poimirlem32  37639  ismtyres  37795  ispridlc  38057  iss2  38319  paddss1  39804  paddss2  39805  lspindp5  41757  sn-sup2  42472  sn-sup3d  42473  dffltz  42615  pw2f1ocnv  43019  onsupmaxb  43221  naddwordnexlem2  43380  ss2iundf  43641  iunrelexp0  43684  gneispace0nelrn3  44124  nzss  44299  onfrALTlem3  44527  onfrALTlem2  44529  sspwtr  44803  sspwtrALT  44804  sspwtrALT2  44805  pwtrVD  44806  pwtrrVD  44807  suctrALT2VD  44818  suctrALT2  44819  onfrALTlem3VD  44869  onfrALTlem2VD  44871  relpmin  44935  relpfrlem  44936  ssclaxsep  44965  omssaxinf2  44971  iinssf  45125  qndenserrnopnlem  46288  dfaimafn  47159  sprsymrelfolem2  47487  mgmplusfreseq  48146  gsumlsscl  48361  lincfsuppcl  48395  linccl  48396  onsetrec  49690