Theorem ssel 3929

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3920

This theorem is referenced by:  ssel2  3930  sseli  3931  sseld  3934  sstr2OLD  3943  nelss  4001  ssrexf  4002  ssralvOLD  4008  ssrexvOLD  4009  ralssOLD  4012  rexssOLD  4013  ssconb  4093  sscon  4094  ssdif  4095  unss1  4136  ssrin  4193  difin2  4252  reuss2  4277  reupick  4280  elpwunsn  4636  sssn  4777  uniss  4866  ss2iun  4960  ssiun  4995  iinss  5005  disjss2  5062  disjss1  5065  pwnss  5291  sspwb  5392  ssopab2bw  5490  ssopab2b  5492  pwssun  5511  xpss12  5634  frinxp  5702  ssrel  5726  ssrel2  5728  ssrelrel  5739  dmss  5845  elreldm  5877  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  relssres  5973  iss  5986  resopab2  5987  imadifssran  6100  ssrnres  6127  dfco2a  6195  cores  6198  oneqmini  6360  sucssel  6404  onssneli  6424  onssnel2i  6425  funssres  6526  fununi  6557  dfimafn  6885  funimass4  6887  funimass3  6988  dff3  7034  dff4  7035  funfvima2  7167  funfvima3  7172  f1elima  7200  isomin  7274  isofrlem  7277  riotass2  7336  ssoprab2b  7418  eqoprab2bw  7419  resoprab2  7468  ssorduni  7715  onint  7726  oninton  7731  ssnlim  7819  mptcnfimad  7921  releldm2  7978  orderseqlem  8090  dmtpos  8171  onfununi  8264  tz7.48lem  8363  tz7.49  8367  omeulem1  8500  omeulem2  8501  omsmolem  8575  omsmo  8576  ss2ixp  8837  boxriin  8867  unblem1  9181  unblem3  9183  fiint  9216  fiintOLD  9217  inf3lem2  9525  cantnflem2  9586  tcel  9641  tz9.13  9687  rankr1ag  9698  rankpwi  9719  rankelb  9720  bndrank  9737  cardlim  9868  carduni  9877  acni2  9940  dfac12r  10041  cfub  10143  cflim2  10157  fin1a2lem9  10302  axdc3lem2  10345  axdclem2  10414  gch2  10569  eltsk2g  10645  suplem1pr  10946  negn0  11549  negf1o  11550  negfi  12074  lbreu  12075  lbinf  12078  sup2  12081  sup3  12082  infm3  12084  infregelb  12109  uzwo  12812  eqreznegel  12835  xrsupsslem  13209  xrinfmsslem  13210  supxrpnf  13220  supxrunb1  13221  supxrunb2  13222  iccsupr  13345  ssnn0fi  13892  incexclem  15743  fprodmodd  15904  sumeven  16298  sumodd  16299  gcdcllem1  16410  lcmfnnval  16535  lcmfnncl  16540  dvdslcmf  16542  lcmfunsnlem2lem2  16550  lcmfdvdsb  16554  lubel  18420  clatleglb  18424  smndex1mgm  18781  smndex1sgrp  18782  smndex1mnd  18784  mulgpropd  18995  sylow2a  19498  efgi2  19604  ellspsn6  20897  rnglidlmcl  21123  submabas  22463  pmatcollpw3lem  22668  elcls2  22959  isclo2  22973  cmpsublem  23284  cmpsub  23285  hauscmplem  23291  1stcelcls  23346  llyss  23364  nllyss  23365  txkgen  23537  nrmr0reg  23634  uffix  23806  ufinffr  23814  ufilen  23815  fmfnfmlem2  23840  alexsubALTlem2  23933  alexsubALT  23936  metrest  24410  iccntr  24708  reconnlem2  24714  clmneg1  24980  clmvscom  24988  caubl  25206  dvply2g  26190  ulmss  26304  nofv  27567  nocvxminlem  27688  nocvxmin  27689  axcontlem4  28912  ocsh  31227  ococss  31237  shorth  31239  spansnss2  31519  h1datomi  31525  pjss2i  31624  pjssmii  31625  pjorthcoi  32113  pj3si  32151  ssrelf  32560  dfimafnf  32579  funimass4f  32580  mptssALT  32618  1stpreima  32649  2ndpreima  32650  indpi1  32803  isprmidlc  33384  ordtconnlem1  33891  bnj518  34853  nummin  35058  tz9.1regs  35067  cvmlift2lem1  35275  satffunlem2lem1  35377  satfvel  35385  dfon2lem6  35762  limsucncmpi  36419  finxpreclem4  37368  poimirlem3  37603  poimirlem29  37629  poimirlem32  37632  ismtyres  37788  ispridlc  38050  iss2  38312  paddss1  39796  paddss2  39797  lspindp5  41749  sn-sup2  42464  sn-sup3d  42465  dffltz  42607  pw2f1ocnv  43010  onsupmaxb  43212  naddwordnexlem2  43371  ss2iundf  43632  iunrelexp0  43675  gneispace0nelrn3  44115  nzss  44290  onfrALTlem3  44518  onfrALTlem2  44520  sspwtr  44794  sspwtrALT  44795  sspwtrALT2  44796  pwtrVD  44797  pwtrrVD  44798  suctrALT2VD  44809  suctrALT2  44810  onfrALTlem3VD  44860  onfrALTlem2VD  44862  relpmin  44926  relpfrlem  44927  ssclaxsep  44956  omssaxinf2  44962  iinssf  45116  qndenserrnopnlem  46278  dfaimafn  47149  sprsymrelfolem2  47477  mgmplusfreseq  48149  gsumlsscl  48364  lincfsuppcl  48398  linccl  48399  onsetrec  49693