Theorem ssel 3975

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ssel2  3977  sseli  3978  sseld  3981  sstr2  3989  nelss  4047  ssrexf  4048  ssralv  4050  ssrexv  4051  ralss  4054  rexss  4055  ssconb  4137  sscon  4138  ssdif  4139  unss1  4179  ssrin  4233  difin2  4291  reuss2  4315  reupick  4318  elpwunsn  4687  sssn  4829  uniss  4916  ss2iun  5015  ssiun  5049  iinss  5059  disjss2  5116  disjss1  5119  pwnss  5349  sspwb  5449  ssopab2bw  5547  ssopab2b  5549  pwssun  5571  xpss12  5691  frinxp  5758  ssrel  5782  ssrelOLD  5783  ssrel2  5785  ssrelrel  5796  dmss  5902  elreldm  5934  dmcosseq  5972  relssres  6022  iss  6035  resopab2  6036  ssrnres  6177  dfco2a  6245  cores  6248  oneqmini  6416  sucssel  6459  onssneli  6480  onssnel2i  6481  funssres  6592  fununi  6623  dfimafn  6954  funimass4  6956  funimass3  7055  dff3  7101  dff4  7102  funfvima2  7235  funfvima3  7240  f1elima  7264  isomin  7336  isofrlem  7339  riotass2  7398  ssoprab2b  7480  eqoprab2bw  7481  resoprab2  7529  ssorduni  7768  onint  7780  oninton  7785  ssnlim  7877  releldm2  8031  orderseqlem  8145  dmtpos  8225  wfrlem10OLD  8320  onfununi  8343  tz7.48lem  8443  tz7.49  8447  omeulem1  8584  omeulem2  8585  omsmolem  8658  omsmo  8659  ss2ixp  8906  boxriin  8936  onomeneqOLD  9231  unblem1  9297  unblem3  9299  fiint  9326  inf3lem2  9626  cantnflem2  9687  tcel  9742  tz9.13  9788  rankr1ag  9799  rankpwi  9820  rankelb  9821  bndrank  9838  cardlim  9969  carduni  9978  acni2  10043  dfac12r  10143  cfub  10246  cflim2  10260  fin1a2lem9  10405  axdc3lem2  10448  axdclem2  10517  gch2  10672  eltsk2g  10748  suplem1pr  11049  negn0  11645  negf1o  11646  negfi  12165  lbreu  12166  lbinf  12169  sup2  12172  sup3  12173  infm3  12175  infregelb  12200  uzwo  12897  eqreznegel  12920  xrsupsslem  13288  xrinfmsslem  13289  supxrpnf  13299  supxrunb1  13300  supxrunb2  13301  iccsupr  13421  ssnn0fi  13952  incexclem  15784  fprodmodd  15943  sumeven  16332  sumodd  16333  gcdcllem1  16442  lcmfnnval  16563  lcmfnncl  16568  dvdslcmf  16570  lcmfunsnlem2lem2  16578  lcmfdvdsb  16582  lubel  18469  clatleglb  18473  smndex1mgm  18790  smndex1sgrp  18791  smndex1mnd  18793  mulgpropd  18998  sylow2a  19489  efgi2  19595  lspsnel6  20610  submabas  22087  pmatcollpw3lem  22292  elcls2  22585  isclo2  22599  cmpsublem  22910  cmpsub  22911  hauscmplem  22917  1stcelcls  22972  llyss  22990  nllyss  22991  txkgen  23163  nrmr0reg  23260  uffix  23432  ufinffr  23440  ufilen  23441  fmfnfmlem2  23466  alexsubALTlem2  23559  alexsubALT  23562  metrest  24040  iccntr  24344  reconnlem2  24350  clmneg1  24605  clmvscom  24613  caubl  24832  ulmss  25916  nofv  27167  nocvxminlem  27286  nocvxmin  27287  axcontlem4  28263  ocsh  30574  ococss  30584  shorth  30586  spansnss2  30866  h1datomi  30872  pjss2i  30971  pjssmii  30972  pjorthcoi  31460  pj3si  31498  ssrelf  31882  dfimafnf  31898  funimass4f  31899  mptssALT  31938  1stpreima  31966  2ndpreima  31967  isprmidlc  32611  ordtconnlem1  32973  indpi1  33087  bnj518  33966  nummin  34163  cvmlift2lem1  34362  satffunlem2lem1  34464  satfvel  34472  dfon2lem6  34835  limsucncmpi  35422  finxpreclem4  36367  poimirlem3  36583  poimirlem29  36609  poimirlem32  36612  ismtyres  36768  ispridlc  37030  iss2  37305  paddss1  38780  paddss2  38781  lspindp5  40733  sn-sup2  41430  dffltz  41464  pw2f1ocnv  41864  onsupmaxb  42076  naddwordnexlem2  42237  ss2iundf  42498  iunrelexp0  42541  gneispace0nelrn3  42981  nzss  43164  onfrALTlem3  43393  onfrALTlem2  43395  sspwtr  43670  sspwtrALT  43671  sspwtrALT2  43672  pwtrVD  43673  pwtrrVD  43674  suctrALT2VD  43685  suctrALT2  43686  onfrALTlem3VD  43736  onfrALTlem2VD  43738  iinssf  43915  qndenserrnopnlem  45098  dfaimafn  45958  sprsymrelfolem2  46246  mgmplusfreseq  46628  rnglidlmcl  46833  gsumlsscl  47144  lincfsuppcl  47178  linccl  47179  onsetrec  47837