Theorem ssel 3909

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-ss 3900

This theorem is referenced by:  ssel2  3910  sseli  3911  sseld  3914  nelss  3980  ssrexf  3981  ralssOLD  3989  rexssOLD  3990  rabss2  4008  ssconb  4072  sscon  4073  ssdif  4074  unss1  4114  ssrin  4170  difin2  4229  reuss2  4254  reupick  4257  elpwunsn  4616  sssn  4757  uniss  4846  ss2iun  4940  ssiun  4976  iinss  4986  disjss2  5042  disjss1  5045  pwnss  5280  sspwb  5388  ssopab2bw  5489  ssopab2b  5491  pwssun  5510  xpss12  5633  frinxp  5701  ssrel  5726  ssrel2  5728  ssrelrel  5739  dmss  5844  elreldm  5877  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  relssres  5974  iss  5987  resopab2  5988  imadifssran  6102  ssrnres  6129  dfco2a  6197  cores  6200  oneqmini  6363  sucssel  6407  onssneli  6427  onssnel2i  6428  funssres  6529  fununi  6560  dfimafn  6889  funimass4  6891  funimass3  6995  dff3  7041  dff4  7042  funfvima2  7175  funfvima3  7180  f1elima  7207  isomin  7281  isofrlem  7284  riotass2  7343  ssoprab2b  7425  eqoprab2bw  7426  resoprab2  7475  ssorduni  7722  onint  7733  oninton  7738  ssnlim  7826  mptcnfimad  7928  releldm2  7985  orderseqlem  8097  dmtpos  8178  onfununi  8271  tz7.48lem  8370  tz7.49  8374  omeulem1  8507  omeulem2  8508  omsmolem  8583  omsmo  8584  ss2ixp  8848  boxriin  8878  unblem1  9192  unblem3  9194  fiint  9227  inf3lem2  9541  cantnflem2  9602  tcel  9655  tz9.13  9706  rankr1ag  9717  rankpwi  9738  rankelb  9739  bndrank  9756  cardlim  9887  carduni  9896  acni2  9959  dfac12r  10060  cfub  10162  cflim2  10176  fin1a2lem9  10321  axdc3lem2  10364  axdclem2  10433  gch2  10589  eltsk2g  10665  suplem1pr  10966  negn0  11570  negf1o  11571  negfi  12096  lbreu  12097  lbinf  12100  sup2  12103  sup3  12104  infm3  12106  infregelb  12131  indpi1  12164  uzwo  12852  eqreznegel  12875  xrsupsslem  13250  xrinfmsslem  13251  supxrpnf  13261  supxrunb1  13262  supxrunb2  13263  iccsupr  13386  ssnn0fi  13938  incexclem  15792  fprodmodd  15953  sumeven  16347  sumodd  16348  gcdcllem1  16459  lcmfnnval  16584  lcmfnncl  16589  dvdslcmf  16591  lcmfunsnlem2lem2  16599  lcmfdvdsb  16603  lubel  18471  clatleglb  18475  smndex1mgm  18869  smndex1sgrp  18870  smndex1mnd  18872  mulgpropd  19083  sylow2a  19585  efgi2  19691  ellspsn6  20984  rnglidlmcl  21209  submabas  22561  pmatcollpw3lem  22766  elcls2  23057  isclo2  23071  cmpsublem  23382  cmpsub  23383  hauscmplem  23389  1stcelcls  23444  llyss  23462  nllyss  23463  txkgen  23635  nrmr0reg  23732  uffix  23904  ufinffr  23912  ufilen  23913  fmfnfmlem2  23938  alexsubALTlem2  24031  alexsubALT  24034  metrest  24507  iccntr  24805  reconnlem2  24811  clmneg1  25067  clmvscom  25075  caubl  25293  dvply2g  26269  ulmss  26380  nofv  27639  nocvxminlem  27764  nocvxmin  27765  axcontlem4  29054  ocsh  31372  ococss  31382  shorth  31384  spansnss2  31664  h1datomi  31670  pjss2i  31769  pjssmii  31770  pjorthcoi  32258  pj3si  32296  ssrelf  32707  dfimafnf  32728  funimass4f  32729  mptssALT  32766  1stpreima  32799  2ndpreima  32800  isprmidlc  33530  ordtconnlem1  34108  bnj518  35068  fissorduni  35271  nummin  35274  tz9.1regs  35315  cvmlift2lem1  35530  satffunlem2lem1  35632  satfvel  35640  dfon2lem6  36014  limsucncmpi  36673  finxpreclem4  37756  poimirlem3  37990  poimirlem29  38016  poimirlem32  38019  ismtyres  38175  ispridlc  38437  iss2  38711  paddss1  40309  paddss2  40310  lspindp5  42262  sn-sup2  42981  sn-sup3d  42982  dffltz  43084  pw2f1ocnv  43482  onsupmaxb  43684  naddwordnexlem2  43843  ss2iundf  44103  iunrelexp0  44146  gneispace0nelrn3  44586  nzss  44761  onfrALTlem3  44988  onfrALTlem2  44990  sspwtr  45264  sspwtrALT  45265  sspwtrALT2  45266  pwtrVD  45267  pwtrrVD  45268  suctrALT2VD  45279  suctrALT2  45280  onfrALTlem3VD  45330  onfrALTlem2VD  45332  relpmin  45396  relpfrlem  45397  ssclaxsep  45426  omssaxinf2  45432  iinssf  45585  qndenserrnopnlem  46740  dfaimafn  47628  sprsymrelfolem2  47968  mgmplusfreseq  48656  gsumlsscl  48871  lincfsuppcl  48904  linccl  48905  onsetrec  50198