Theorem ssel 3925

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2809  df-ss 3916

This theorem is referenced by:  ssel2  3926  sseli  3927  sseld  3930  sstr2OLD  3939  nelss  3997  ssrexf  3998  ssralvOLD  4004  ssrexvOLD  4005  ralssOLD  4008  rexssOLD  4009  rabss2  4027  ssconb  4092  sscon  4093  ssdif  4094  unss1  4135  ssrin  4192  difin2  4251  reuss2  4276  reupick  4279  elpwunsn  4639  sssn  4780  uniss  4869  ss2iun  4963  ssiun  5000  iinss  5010  disjss2  5066  disjss1  5069  pwnss  5295  sspwb  5395  ssopab2bw  5493  ssopab2b  5495  pwssun  5514  xpss12  5637  frinxp  5705  ssrel  5730  ssrel2  5732  ssrelrel  5743  dmss  5849  elreldm  5882  dmcosseq  5925  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  relssres  5979  iss  5992  resopab2  5993  imadifssran  6107  ssrnres  6134  dfco2a  6202  cores  6205  oneqmini  6368  sucssel  6412  onssneli  6432  onssnel2i  6433  funssres  6534  fununi  6565  dfimafn  6894  funimass4  6896  funimass3  6997  dff3  7043  dff4  7044  funfvima2  7175  funfvima3  7180  f1elima  7207  isomin  7281  isofrlem  7284  riotass2  7343  ssoprab2b  7425  eqoprab2bw  7426  resoprab2  7475  ssorduni  7722  onint  7733  oninton  7738  ssnlim  7826  mptcnfimad  7928  releldm2  7985  orderseqlem  8097  dmtpos  8178  onfununi  8271  tz7.48lem  8370  tz7.49  8374  omeulem1  8507  omeulem2  8508  omsmolem  8583  omsmo  8584  ss2ixp  8846  boxriin  8876  unblem1  9190  unblem3  9192  fiint  9225  inf3lem2  9536  cantnflem2  9597  tcel  9650  tz9.13  9701  rankr1ag  9712  rankpwi  9733  rankelb  9734  bndrank  9751  cardlim  9882  carduni  9891  acni2  9954  dfac12r  10055  cfub  10157  cflim2  10171  fin1a2lem9  10316  axdc3lem2  10359  axdclem2  10428  gch2  10584  eltsk2g  10660  suplem1pr  10961  negn0  11564  negf1o  11565  negfi  12089  lbreu  12090  lbinf  12093  sup2  12096  sup3  12097  infm3  12099  infregelb  12124  uzwo  12822  eqreznegel  12845  xrsupsslem  13220  xrinfmsslem  13221  supxrpnf  13231  supxrunb1  13232  supxrunb2  13233  iccsupr  13356  ssnn0fi  13906  incexclem  15757  fprodmodd  15918  sumeven  16312  sumodd  16313  gcdcllem1  16424  lcmfnnval  16549  lcmfnncl  16554  dvdslcmf  16556  lcmfunsnlem2lem2  16564  lcmfdvdsb  16568  lubel  18435  clatleglb  18439  smndex1mgm  18830  smndex1sgrp  18831  smndex1mnd  18833  mulgpropd  19044  sylow2a  19546  efgi2  19652  ellspsn6  20943  rnglidlmcl  21169  submabas  22520  pmatcollpw3lem  22725  elcls2  23016  isclo2  23030  cmpsublem  23341  cmpsub  23342  hauscmplem  23348  1stcelcls  23403  llyss  23421  nllyss  23422  txkgen  23594  nrmr0reg  23691  uffix  23863  ufinffr  23871  ufilen  23872  fmfnfmlem2  23897  alexsubALTlem2  23990  alexsubALT  23993  metrest  24466  iccntr  24764  reconnlem2  24770  clmneg1  25036  clmvscom  25044  caubl  25262  dvply2g  26246  ulmss  26360  nofv  27623  nocvxminlem  27744  nocvxmin  27745  axcontlem4  28989  ocsh  31307  ococss  31317  shorth  31319  spansnss2  31599  h1datomi  31605  pjss2i  31704  pjssmii  31705  pjorthcoi  32193  pj3si  32231  ssrelf  32642  dfimafnf  32663  funimass4f  32664  mptssALT  32702  1stpreima  32735  2ndpreima  32736  indpi1  32890  isprmidlc  33477  ordtconnlem1  34030  bnj518  34991  fissorduni  35195  nummin  35198  tz9.1regs  35239  cvmlift2lem1  35445  satffunlem2lem1  35547  satfvel  35555  dfon2lem6  35929  limsucncmpi  36588  finxpreclem4  37538  poimirlem3  37763  poimirlem29  37789  poimirlem32  37792  ismtyres  37948  ispridlc  38210  iss2  38476  paddss1  40016  paddss2  40017  lspindp5  41969  sn-sup2  42688  sn-sup3d  42689  dffltz  42819  pw2f1ocnv  43221  onsupmaxb  43423  naddwordnexlem2  43582  ss2iundf  43842  iunrelexp0  43885  gneispace0nelrn3  44325  nzss  44500  onfrALTlem3  44727  onfrALTlem2  44729  sspwtr  45003  sspwtrALT  45004  sspwtrALT2  45005  pwtrVD  45006  pwtrrVD  45007  suctrALT2VD  45018  suctrALT2  45019  onfrALTlem3VD  45069  onfrALTlem2VD  45071  relpmin  45135  relpfrlem  45136  ssclaxsep  45165  omssaxinf2  45171  iinssf  45324  qndenserrnopnlem  46483  dfaimafn  47353  sprsymrelfolem2  47681  mgmplusfreseq  48353  gsumlsscl  48568  lincfsuppcl  48601  linccl  48602  onsetrec  49895