Theorem ssel 3910

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssel2  3912  sseli  3913  sseld  3916  sstr2  3924  nelss  3980  ssrexf  3981  ssralv  3983  ssrexv  3984  ralss  3987  rexss  3988  ssconb  4068  sscon  4069  ssdif  4070  unss1  4109  ssrin  4164  difin2  4222  reuss2  4246  reupick  4249  elpwunsn  4616  sssn  4756  uniss  4844  ss2iun  4939  ssiun  4972  iinss  4982  disjss2  5038  disjss1  5041  pwnss  5267  sspwb  5359  ssopab2bw  5453  ssopab2b  5455  pwssun  5476  xpss12  5595  frinxp  5660  ssrel  5683  ssrel2  5685  ssrelrel  5695  dmss  5800  elreldm  5833  dmcosseq  5871  relssres  5921  iss  5932  resopab2  5933  ssrnres  6070  dfco2a  6139  cores  6142  oneqmini  6302  sucssel  6343  onssneli  6361  onssnel2i  6362  funssres  6462  fununi  6493  dfimafn  6814  funimass4  6816  funimass3  6913  dff3  6958  dff4  6959  funfvima2  7089  funfvima3  7094  f1elima  7117  isomin  7188  isofrlem  7191  riotass2  7243  ssoprab2b  7322  eqoprab2bw  7323  resoprab2  7371  ssorduni  7606  onint  7617  oninton  7622  ssnlim  7707  releldm2  7857  dmtpos  8025  wfrlem10OLD  8120  onfununi  8143  tz7.48lem  8242  tz7.49  8246  omeulem1  8375  omeulem2  8376  omsmolem  8447  omsmo  8448  ss2ixp  8656  boxriin  8686  onomeneq  8943  unblem1  8996  unblem3  8998  fiint  9021  inf3lem2  9317  cantnflem2  9378  trpredmintr  9409  tcel  9434  tz9.13  9480  rankr1ag  9491  rankpwi  9512  rankelb  9513  bndrank  9530  cardlim  9661  carduni  9670  acni2  9733  dfac12r  9833  cfub  9936  cflim2  9950  fin1a2lem9  10095  axdc3lem2  10138  axdclem2  10207  gch2  10362  eltsk2g  10438  suplem1pr  10739  negn0  11334  negf1o  11335  negfi  11854  lbreu  11855  lbinf  11858  sup2  11861  sup3  11862  infm3  11864  infregelb  11889  uzwo  12580  eqreznegel  12603  xrsupsslem  12970  xrinfmsslem  12971  supxrpnf  12981  supxrunb1  12982  supxrunb2  12983  iccsupr  13103  ssnn0fi  13633  incexclem  15476  fprodmodd  15635  sumeven  16024  sumodd  16025  gcdcllem1  16134  lcmfnnval  16257  lcmfnncl  16262  dvdslcmf  16264  lcmfunsnlem2lem2  16272  lcmfdvdsb  16276  lubel  18147  clatleglb  18151  smndex1mgm  18461  smndex1sgrp  18462  smndex1mnd  18464  mulgpropd  18660  sylow2a  19139  efgi2  19246  lspsnel6  20171  submabas  21635  pmatcollpw3lem  21840  elcls2  22133  isclo2  22147  cmpsublem  22458  cmpsub  22459  hauscmplem  22465  1stcelcls  22520  llyss  22538  nllyss  22539  txkgen  22711  nrmr0reg  22808  uffix  22980  ufinffr  22988  ufilen  22989  fmfnfmlem2  23014  alexsubALTlem2  23107  alexsubALT  23110  metrest  23586  iccntr  23890  reconnlem2  23896  clmneg1  24151  clmvscom  24159  caubl  24377  ulmss  25461  axcontlem4  27238  ocsh  29546  ococss  29556  shorth  29558  spansnss2  29838  h1datomi  29844  pjss2i  29943  pjssmii  29944  pjorthcoi  30432  pj3si  30470  ssrelf  30856  dfimafnf  30872  funimass4f  30873  mptssALT  30914  1stpreima  30941  2ndpreima  30942  isprmidlc  31525  ordtconnlem1  31776  indpi1  31888  bnj518  32766  nummin  32963  cvmlift2lem1  33164  satffunlem2lem1  33266  satfvel  33274  dfon2lem6  33670  orderseqlem  33728  nofv  33787  nocvxminlem  33899  nocvxmin  33900  limsucncmpi  34561  finxpreclem4  35492  poimirlem3  35707  poimirlem29  35733  poimirlem32  35736  ismtyres  35893  ispridlc  36155  iss2  36406  paddss1  37758  paddss2  37759  lspindp5  39711  sn-sup2  40360  dffltz  40387  pw2f1ocnv  40775  ss2iundf  41156  iunrelexp0  41199  gneispace0nelrn3  41641  nzss  41824  onfrALTlem3  42053  onfrALTlem2  42055  sspwtr  42330  sspwtrALT  42331  sspwtrALT2  42332  pwtrVD  42333  pwtrrVD  42334  suctrALT2VD  42345  suctrALT2  42346  onfrALTlem3VD  42396  onfrALTlem2VD  42398  iinssf  42576  qndenserrnopnlem  43728  dfaimafn  44544  sprsymrelfolem2  44833  mgmplusfreseq  45215  gsumlsscl  45607  lincfsuppcl  45642  linccl  45643  onsetrec  46299