Theorem ssel 3916

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 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 613	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2813	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2813	. . 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 3890

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 2812  df-ss 3907

This theorem is referenced by:  ssel2  3917  sseli  3918  sseld  3921  sstr2OLD  3930  nelss  3988  ssrexf  3989  ssralvOLD  3995  ssrexvOLD  3996  ralssOLD  3999  rexssOLD  4000  rabss2  4018  ssconb  4083  sscon  4084  ssdif  4085  unss1  4126  ssrin  4183  difin2  4242  reuss2  4267  reupick  4270  elpwunsn  4629  sssn  4770  uniss  4859  ss2iun  4953  ssiun  4990  iinss  5000  disjss2  5056  disjss1  5059  pwnss  5290  sspwb  5397  ssopab2bw  5496  ssopab2b  5498  pwssun  5517  xpss12  5640  frinxp  5708  ssrel  5733  ssrel2  5735  ssrelrel  5746  dmss  5852  elreldm  5885  dmcosseq  5928  dmcosseqOLD  5929  dmcosseqOLDOLD  5930  relssres  5982  iss  5995  resopab2  5996  imadifssran  6110  ssrnres  6137  dfco2a  6205  cores  6208  oneqmini  6371  sucssel  6415  onssneli  6435  onssnel2i  6436  funssres  6537  fununi  6568  dfimafn  6897  funimass4  6899  funimass3  7001  dff3  7047  dff4  7048  funfvima2  7180  funfvima3  7185  f1elima  7212  isomin  7286  isofrlem  7289  riotass2  7348  ssoprab2b  7430  eqoprab2bw  7431  resoprab2  7480  ssorduni  7727  onint  7738  oninton  7743  ssnlim  7831  mptcnfimad  7933  releldm2  7990  orderseqlem  8101  dmtpos  8182  onfununi  8275  tz7.48lem  8374  tz7.49  8378  omeulem1  8511  omeulem2  8512  omsmolem  8587  omsmo  8588  ss2ixp  8852  boxriin  8882  unblem1  9196  unblem3  9198  fiint  9231  inf3lem2  9544  cantnflem2  9605  tcel  9658  tz9.13  9709  rankr1ag  9720  rankpwi  9741  rankelb  9742  bndrank  9759  cardlim  9890  carduni  9899  acni2  9962  dfac12r  10063  cfub  10165  cflim2  10179  fin1a2lem9  10324  axdc3lem2  10367  axdclem2  10436  gch2  10592  eltsk2g  10668  suplem1pr  10969  negn0  11573  negf1o  11574  negfi  12099  lbreu  12100  lbinf  12103  sup2  12106  sup3  12107  infm3  12109  infregelb  12134  indpi1  12167  uzwo  12855  eqreznegel  12878  xrsupsslem  13253  xrinfmsslem  13254  supxrpnf  13264  supxrunb1  13265  supxrunb2  13266  iccsupr  13389  ssnn0fi  13941  incexclem  15795  fprodmodd  15956  sumeven  16350  sumodd  16351  gcdcllem1  16462  lcmfnnval  16587  lcmfnncl  16592  dvdslcmf  16594  lcmfunsnlem2lem2  16602  lcmfdvdsb  16606  lubel  18474  clatleglb  18478  smndex1mgm  18872  smndex1sgrp  18873  smndex1mnd  18875  mulgpropd  19086  sylow2a  19588  efgi2  19694  ellspsn6  20983  rnglidlmcl  21209  submabas  22556  pmatcollpw3lem  22761  elcls2  23052  isclo2  23066  cmpsublem  23377  cmpsub  23378  hauscmplem  23384  1stcelcls  23439  llyss  23457  nllyss  23458  txkgen  23630  nrmr0reg  23727  uffix  23899  ufinffr  23907  ufilen  23908  fmfnfmlem2  23933  alexsubALTlem2  24026  alexsubALT  24029  metrest  24502  iccntr  24800  reconnlem2  24806  clmneg1  25062  clmvscom  25070  caubl  25288  dvply2g  26264  ulmss  26378  nofv  27638  nocvxminlem  27763  nocvxmin  27764  axcontlem4  29053  ocsh  31372  ococss  31382  shorth  31384  spansnss2  31664  h1datomi  31670  pjss2i  31769  pjssmii  31770  pjorthcoi  32258  pj3si  32296  ssrelf  32706  dfimafnf  32727  funimass4f  32728  mptssALT  32765  1stpreima  32798  2ndpreima  32799  isprmidlc  33525  ordtconnlem1  34087  bnj518  35047  fissorduni  35252  nummin  35255  tz9.1regs  35297  cvmlift2lem1  35503  satffunlem2lem1  35605  satfvel  35613  dfon2lem6  35987  limsucncmpi  36646  finxpreclem4  37727  poimirlem3  37961  poimirlem29  37987  poimirlem32  37990  ismtyres  38146  ispridlc  38408  iss2  38682  paddss1  40280  paddss2  40281  lspindp5  42233  sn-sup2  42953  sn-sup3d  42954  dffltz  43084  pw2f1ocnv  43486  onsupmaxb  43688  naddwordnexlem2  43847  ss2iundf  44107  iunrelexp0  44150  gneispace0nelrn3  44590  nzss  44765  onfrALTlem3  44992  onfrALTlem2  44994  sspwtr  45268  sspwtrALT  45269  sspwtrALT2  45270  pwtrVD  45271  pwtrrVD  45272  suctrALT2VD  45283  suctrALT2  45284  onfrALTlem3VD  45334  onfrALTlem2VD  45336  relpmin  45400  relpfrlem  45401  ssclaxsep  45430  omssaxinf2  45436  iinssf  45589  qndenserrnopnlem  46746  dfaimafn  47628  sprsymrelfolem2  47968  mgmplusfreseq  48656  gsumlsscl  48871  lincfsuppcl  48904  linccl  48905  onsetrec  50198