Theorem ssel 3930

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1558   = wceq 1560  ∃wex 1799   ∈ wcel 2142   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837  df-ss 3921

This theorem is referenced by:  ssel2  3931  sseli  3932  sseld  3935  nelss  4002  ssrexf  4003  ralssOLD  4011  rexssOLD  4012  rabss2  4030  ssconb  4095  sscon  4096  ssdif  4097  unss1  4137  ssrin  4193  difin2  4253  reuss2  4278  reupick  4281  elpwunsn  4643  sssn  4784  uniss  4873  ss2iun  4968  ssiun  5004  iinss  5014  disjss2  5070  disjss1  5073  pwnss  5308  sspwb  5416  ssopab2bw  5518  ssopab2b  5520  pwssun  5539  xpss12  5662  frinxp  5730  ssrel  5755  ssrel2  5757  ssrelrel  5768  dmss  5878  elreldm  5911  dmcosseq  5954  dmcosseqOLD  5955  dmcosseqOLDOLD  5956  relssres  6008  iss  6024  resopab2  6025  imadifssran  6136  ssrnres  6164  dfco2a  6233  cores  6236  oneqmini  6399  sucssel  6443  onssneli  6463  onssnel2i  6464  funssres  6565  fununi  6596  dfimafn  6929  funimass4  6931  funimass3  7035  dff3  7081  dff4  7082  funfvima2  7215  funfvima3  7220  f1elima  7247  isomin  7321  isofrlem  7324  riotass2  7383  ssoprab2b  7465  eqoprab2bw  7466  resoprab2  7515  ssorduni  7762  onint  7773  oninton  7778  ssnlim  7866  mptcnfimad  7967  releldm2  8024  orderseqlem  8137  dmtpos  8218  onfununi  8312  tz7.48lem  8412  tz7.49  8416  omeulem1  8551  omeulem2  8552  omsmolem  8627  omsmo  8628  ss2ixp  8892  boxriin  8922  unblem1  9236  unblem3  9238  fiint  9271  inf3lem2  9584  cantnflem2  9645  tcel  9698  tz9.13  9749  rankr1ag  9760  rankpwi  9781  rankelb  9782  bndrank  9799  cardlim  9930  carduni  9939  acni2  10002  dfac12r  10103  cfub  10205  cflim2  10220  fin1a2lem9  10365  axdc3lem2  10408  axdclem2  10477  gch2  10633  eltsk2g  10709  suplem1pr  11010  negn0  11616  negf1o  11617  negfi  12141  lbreu  12142  lbinf  12145  sup2  12148  sup3  12149  infm3  12151  infregelb  12176  indpi1  12209  uzwo  12912  eqreznegel  12935  xrsupsslem  13310  xrinfmsslem  13311  supxrpnf  13321  supxrunb1  13322  supxrunb2  13323  iccsupr  13446  ssnn0fi  13998  incexclem  15866  fprodmodd  16027  sumeven  16421  sumodd  16422  gcdcllem1  16533  lcmfnnval  16658  lcmfnncl  16663  dvdslcmf  16665  lcmfunsnlem2lem2  16673  lcmfdvdsb  16677  lubel  18546  clatleglb  18550  smndex1mgm  18944  smndex1sgrp  18945  smndex1mnd  18947  mulgpropd  19158  sylow2a  19659  efgi2  19765  ellspsn6  21058  rnglidlmcl  21283  submabas  22635  pmatcollpw3lem  22840  elcls2  23131  isclo2  23145  cmpsublem  23456  cmpsub  23457  hauscmplem  23463  1stcelcls  23518  llyss  23536  nllyss  23537  txkgen  23709  nrmr0reg  23806  uffix  23978  ufinffr  23986  ufilen  23987  fmfnfmlem2  24012  alexsubALTlem2  24105  alexsubALT  24108  metrest  24581  iccntr  24879  reconnlem2  24885  clmneg1  25141  clmvscom  25149  caubl  25367  dvply2g  26346  ulmss  26457  nofv  27718  nocvxminlem  27844  nocvxmin  27845  axcontlem4  29165  ocsh  31483  ococss  31493  shorth  31495  spansnss2  31775  h1datomi  31781  pjss2i  31880  pjssmii  31881  pjorthcoi  32369  pj3si  32407  ssrelf  32814  dfimafnf  32835  funimass4f  32836  mptssALT  32873  1stpreima  32906  2ndpreima  32907  isprmidlc  33630  ordtconnlem1  34218  bnj518  35178  fissorduni  35382  nummin  35386  tz9.1regs  35427  cvmlift2lem1  35649  satffunlem2lem1  35751  satfvel  35759  dfon2lem6  36133  limsucncmpi  36802  finxpreclem4  37885  poimirlem3  38119  poimirlem29  38145  poimirlem32  38148  ismtyres  38304  ispridlc  38566  iss2  38840  paddss1  40438  paddss2  40439  lspindp5  42391  sn-sup2  43110  sn-sup3d  43111  dffltz  43213  pw2f1ocnv  43611  onsupmaxb  43813  naddwordnexlem2  43972  ss2iundf  44232  iunrelexp0  44275  gneispace0nelrn3  44715  nzss  44890  onfrALTlem3  45117  onfrALTlem2  45119  sspwtr  45393  sspwtrALT  45394  sspwtrALT2  45395  pwtrVD  45396  pwtrrVD  45397  suctrALT2VD  45408  suctrALT2  45409  onfrALTlem3VD  45459  onfrALTlem2VD  45461  relpmin  45525  relpfrlem  45526  ssclaxsep  45555  omssaxinf2  45561  iinssf  45713  qndenserrnopnlem  46868  dfaimafn  47756  sprsymrelfolem2  48096  mgmplusfreseq  48784  gsumlsscl  48999  lincfsuppcl  49032  linccl  49033  onsetrec  50326