Theorem ssel 3908

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  ssel2  3910  sseli  3911  sseld  3914  sstr2  3922  nelss  3978  ssrexf  3979  ssralv  3981  ssrexv  3982  ralss  3985  rexss  3986  ssconb  4065  sscon  4066  ssdif  4067  unss1  4106  ssrin  4160  difin2  4216  reuss2  4235  reupick  4239  elpwunsn  4581  sssn  4719  uniss  4808  ss2iun  4899  ssiun  4933  iinss  4943  disjss2  4998  disjss1  5001  pwnss  5215  sspwb  5307  ssopab2bw  5399  ssopab2b  5401  pwssun  5421  xpss12  5534  frinxp  5598  ssrel  5621  ssrel2  5623  ssrelrel  5633  dmss  5735  elreldm  5769  dmcosseq  5809  relssres  5859  iss  5870  resopab2  5871  ssrnres  6002  dfco2a  6066  cores  6069  oneqmini  6210  sucssel  6251  onssneli  6268  onssnel2i  6269  funssres  6368  fununi  6399  dfimafn  6703  funimass4  6705  funimass3  6801  dff3  6843  dff4  6844  funfvima2  6971  funfvima3  6976  f1elima  6999  isomin  7069  isofrlem  7072  riotass2  7123  ssoprab2b  7202  eqoprab2bw  7203  resoprab2  7250  ssorduni  7480  onint  7490  oninton  7495  ssnlim  7579  releldm2  7724  dmtpos  7887  wfrlem10  7947  onfununi  7961  tz7.48lem  8060  tz7.49  8064  omeulem1  8191  omeulem2  8192  omsmolem  8263  omsmo  8264  ss2ixp  8457  boxriin  8487  onomeneq  8693  unblem1  8754  unblem3  8756  fiint  8779  inf3lem2  9076  cantnflem2  9137  tcel  9171  tz9.13  9204  rankr1ag  9215  rankpwi  9236  rankelb  9237  bndrank  9254  cardlim  9385  carduni  9394  acni2  9457  dfac12r  9557  cfub  9660  cflim2  9674  fin1a2lem9  9819  axdc3lem2  9862  axdclem2  9931  gch2  10086  eltsk2g  10162  suplem1pr  10463  negn0  11058  negf1o  11059  negfi  11577  lbreu  11578  lbinf  11581  sup2  11584  sup3  11585  infm3  11587  infregelb  11612  uzwo  12299  eqreznegel  12322  xrsupsslem  12688  xrinfmsslem  12689  supxrpnf  12699  supxrunb1  12700  supxrunb2  12701  iccsupr  12820  ssnn0fi  13348  incexclem  15183  fprodmodd  15343  sumeven  15728  sumodd  15729  gcdcllem1  15838  lcmfnnval  15958  lcmfnncl  15963  dvdslcmf  15965  lcmfunsnlem2lem2  15973  lcmfdvdsb  15977  lubel  17724  clatleglb  17728  smndex1mgm  18064  smndex1sgrp  18065  smndex1mnd  18067  mulgpropd  18261  sylow2a  18736  efgi2  18843  lspsnel6  19759  submabas  21183  pmatcollpw3lem  21388  elcls2  21679  isclo2  21693  cmpsublem  22004  cmpsub  22005  hauscmplem  22011  1stcelcls  22066  llyss  22084  nllyss  22085  txkgen  22257  nrmr0reg  22354  uffix  22526  ufinffr  22534  ufilen  22535  fmfnfmlem2  22560  alexsubALTlem2  22653  alexsubALT  22656  metrest  23131  iccntr  23426  reconnlem2  23432  clmneg1  23687  clmvscom  23695  caubl  23912  ulmss  24992  axcontlem4  26761  ocsh  29066  ococss  29076  shorth  29078  spansnss2  29358  h1datomi  29364  pjss2i  29463  pjssmii  29464  pjorthcoi  29952  pj3si  29990  ssrelf  30379  dfimafnf  30395  funimass4f  30396  mptssALT  30438  1stpreima  30466  2ndpreima  30467  isprmidlc  31031  ordtconnlem1  31277  indpi1  31389  bnj518  32268  nummin  32474  cvmlift2lem1  32662  satffunlem2lem1  32764  satfvel  32772  dfon2lem6  33146  trpredmintr  33183  orderseqlem  33207  nofv  33277  nocvxminlem  33360  nocvxmin  33361  limsucncmpi  33906  finxpreclem4  34811  poimirlem3  35060  poimirlem29  35086  poimirlem32  35089  ismtyres  35246  ispridlc  35508  iss2  35761  paddss1  37113  paddss2  37114  lspindp5  39066  sn-sup2  39594  dffltz  39615  pw2f1ocnv  39978  ss2iundf  40360  iunrelexp0  40403  gneispace0nelrn3  40845  nzss  41021  onfrALTlem3  41250  onfrALTlem2  41252  sspwtr  41527  sspwtrALT  41528  sspwtrALT2  41529  pwtrVD  41530  pwtrrVD  41531  suctrALT2VD  41542  suctrALT2  41543  onfrALTlem3VD  41593  onfrALTlem2VD  41595  iinssf  41775  qndenserrnopnlem  42939  dfaimafn  43721  sprsymrelfolem2  44010  mgmplusfreseq  44393  gsumlsscl  44785  lincfsuppcl  44822  linccl  44823  onsetrec  45237