Theorem ssel 3927

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

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 2811  df-ss 3918

This theorem is referenced by:  ssel2  3928  sseli  3929  sseld  3932  sstr2OLD  3941  nelss  3999  ssrexf  4000  ssralvOLD  4006  ssrexvOLD  4007  ralssOLD  4010  rexssOLD  4011  rabss2  4029  ssconb  4094  sscon  4095  ssdif  4096  unss1  4137  ssrin  4194  difin2  4253  reuss2  4278  reupick  4281  elpwunsn  4641  sssn  4782  uniss  4871  ss2iun  4965  ssiun  5002  iinss  5012  disjss2  5068  disjss1  5071  pwnss  5297  sspwb  5397  ssopab2bw  5495  ssopab2b  5497  pwssun  5516  xpss12  5639  frinxp  5707  ssrel  5732  ssrel2  5734  ssrelrel  5745  dmss  5851  elreldm  5884  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  relssres  5981  iss  5994  resopab2  5995  imadifssran  6109  ssrnres  6136  dfco2a  6204  cores  6207  oneqmini  6370  sucssel  6414  onssneli  6434  onssnel2i  6435  funssres  6536  fununi  6567  dfimafn  6896  funimass4  6898  funimass3  6999  dff3  7045  dff4  7046  funfvima2  7177  funfvima3  7182  f1elima  7209  isomin  7283  isofrlem  7286  riotass2  7345  ssoprab2b  7427  eqoprab2bw  7428  resoprab2  7477  ssorduni  7724  onint  7735  oninton  7740  ssnlim  7828  mptcnfimad  7930  releldm2  7987  orderseqlem  8099  dmtpos  8180  onfununi  8273  tz7.48lem  8372  tz7.49  8376  omeulem1  8509  omeulem2  8510  omsmolem  8585  omsmo  8586  ss2ixp  8848  boxriin  8878  unblem1  9192  unblem3  9194  fiint  9227  inf3lem2  9538  cantnflem2  9599  tcel  9652  tz9.13  9703  rankr1ag  9714  rankpwi  9735  rankelb  9736  bndrank  9753  cardlim  9884  carduni  9893  acni2  9956  dfac12r  10057  cfub  10159  cflim2  10173  fin1a2lem9  10318  axdc3lem2  10361  axdclem2  10430  gch2  10586  eltsk2g  10662  suplem1pr  10963  negn0  11566  negf1o  11567  negfi  12091  lbreu  12092  lbinf  12095  sup2  12098  sup3  12099  infm3  12101  infregelb  12126  uzwo  12824  eqreznegel  12847  xrsupsslem  13222  xrinfmsslem  13223  supxrpnf  13233  supxrunb1  13234  supxrunb2  13235  iccsupr  13358  ssnn0fi  13908  incexclem  15759  fprodmodd  15920  sumeven  16314  sumodd  16315  gcdcllem1  16426  lcmfnnval  16551  lcmfnncl  16556  dvdslcmf  16558  lcmfunsnlem2lem2  16566  lcmfdvdsb  16570  lubel  18437  clatleglb  18441  smndex1mgm  18832  smndex1sgrp  18833  smndex1mnd  18835  mulgpropd  19046  sylow2a  19548  efgi2  19654  ellspsn6  20945  rnglidlmcl  21171  submabas  22522  pmatcollpw3lem  22727  elcls2  23018  isclo2  23032  cmpsublem  23343  cmpsub  23344  hauscmplem  23350  1stcelcls  23405  llyss  23423  nllyss  23424  txkgen  23596  nrmr0reg  23693  uffix  23865  ufinffr  23873  ufilen  23874  fmfnfmlem2  23899  alexsubALTlem2  23992  alexsubALT  23995  metrest  24468  iccntr  24766  reconnlem2  24772  clmneg1  25038  clmvscom  25046  caubl  25264  dvply2g  26248  ulmss  26362  nofv  27625  nocvxminlem  27750  nocvxmin  27751  axcontlem4  29040  ocsh  31358  ococss  31368  shorth  31370  spansnss2  31650  h1datomi  31656  pjss2i  31755  pjssmii  31756  pjorthcoi  32244  pj3si  32282  ssrelf  32693  dfimafnf  32714  funimass4f  32715  mptssALT  32753  1stpreima  32786  2ndpreima  32787  indpi1  32941  isprmidlc  33528  ordtconnlem1  34081  bnj518  35042  fissorduni  35246  nummin  35249  tz9.1regs  35290  cvmlift2lem1  35496  satffunlem2lem1  35598  satfvel  35606  dfon2lem6  35980  limsucncmpi  36639  finxpreclem4  37599  poimirlem3  37824  poimirlem29  37850  poimirlem32  37853  ismtyres  38009  ispridlc  38271  iss2  38537  paddss1  40077  paddss2  40078  lspindp5  42030  sn-sup2  42746  sn-sup3d  42747  dffltz  42877  pw2f1ocnv  43279  onsupmaxb  43481  naddwordnexlem2  43640  ss2iundf  43900  iunrelexp0  43943  gneispace0nelrn3  44383  nzss  44558  onfrALTlem3  44785  onfrALTlem2  44787  sspwtr  45061  sspwtrALT  45062  sspwtrALT2  45063  pwtrVD  45064  pwtrrVD  45065  suctrALT2VD  45076  suctrALT2  45077  onfrALTlem3VD  45127  onfrALTlem2VD  45129  relpmin  45193  relpfrlem  45194  ssclaxsep  45223  omssaxinf2  45229  iinssf  45382  qndenserrnopnlem  46541  dfaimafn  47411  sprsymrelfolem2  47739  mgmplusfreseq  48411  gsumlsscl  48626  lincfsuppcl  48659  linccl  48660  onsetrec  49953