Theorem ssel 3903

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 3897	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 624	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1864	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2836	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2836	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3897

This theorem is used by:  ssel2  3904  sseli  3905  sseld  3908  nelss  3975  ssrexf  3976  rabss2  4001  ssconb  4077  sscon  4078  ssdif  4079  ssrin  4137  unss1  4182  difin2  4245  reuss2  4270  reupick  4273  elpwunsn  4641  sssn  4781  uniss  4874  ss2iun  4969  ssiun  5004  iinss  5014  disjss2  5072  disjss1  5075  pwnss  5312  sspwb  5416  ssopab2bw  5521  ssopab2b  5523  pwssun  5542  xpss12  5665  frinxp  5734  ssrel  5759  ssrel2  5761  ssrelrel  5772  dmss  5884  elreldm  5917  dmcosseq  5960  dmcosseqOLD  5961  relssres  6012  iss  6028  resopab2  6029  dfrn7  6067  ssrnres  6171  imadifssranOLD  6204  imadifssranOLDOLD  6205  dfco2a  6249  cores  6252  oneqmini  6418  sucssel  6462  onssneli  6482  onssnel2i  6483  funssres  6587  fununi  6618  dfimafn  6950  funimass4  6952  funimass3  7056  dff3  7103  dff4  7104  funfvima2  7239  funfvima3  7244  f1elima  7269  isomin  7347  isofrlem  7350  riotass2  7409  ssoprab2b  7491  eqoprab2bw  7492  resoprab2  7541  ssorduni  7795  onint  7806  oninton  7811  ssnlim  7899  mptcnfimad  8000  releldm2  8056  orderseqlem  8178  dmtpos  8260  onfununi  8354  tz7.48lemOLD  8456  tz7.49  8460  omeulem1  8595  omeulem2  8596  omsmolem  8671  omsmo  8672  ss2ixp  8943  boxriin  8973  fissorduni  9287  unblem1  9289  unblem3  9291  fiint  9323  inf3lem2  9635  cantnflem2  9696  tcel  9749  tz9.13  9803  rankr1ag  9815  rankpwi  9837  rankelb  9838  bndrank  9859  cardlim  10058  carduni  10067  acni2  10130  dfac12r  10230  cfub  10331  cflim2  10346  fin1a2lem9  10491  axdc3lem2  10534  axdclem2  10603  gch2  10765  eltsk2g  10841  suplem1pr  11142  negn0  11750  negf1o  11751  negfi  12271  lbreu  12272  lbinf  12275  sup2  12278  sup3  12279  infm3  12281  infregelb  12306  indpi1  12339  uzwo  13043  eqreznegel  13066  xrsupsslem  13442  xrinfmsslem  13443  supxrpnf  13453  supxrunb1  13454  supxrunb2  13455  iccsupr  13578  ssnn0fi  14133  incexclem  16012  fprodmodd  16171  sumeven  16564  sumodd  16565  gcdcllem1  16676  lcmfnnval  16806  lcmfnncl  16811  dvdslcmf  16813  lcmfunsnlem2lem2  16821  lcmfdvdsb  16825  lubel  18695  clatleglb  18699  smndex1mgm  19113  smndex1sgrp  19114  smndex1mnd  19116  mulgpropd  19333  sylow2a  19840  efgi2  19946  ellspsn6  21276  rnglidlmcl  21502  lidlunin0  21522  unichnlidl  21523  isprmidlc  21635  submabas  22900  pmatcollpw3lem  23108  elcls2  23399  isclo2  23413  cmpsublem  23724  cmpsub  23725  hauscmplem  23731  1stcelcls  23787  llyss  23805  nllyss  23806  txkgen  23978  nrmr0reg  24075  uffix  24247  ufinffr  24255  ufilen  24256  fmfnfmlem2  24281  alexsubALTlem2  24374  alexsubALT  24377  metrest  24850  iccntr  25148  reconnlem2  25154  clmneg1  25410  clmvscom  25418  caubl  25636  dvply2g  26613  ulmss  26731  nofv  28021  nocvxminlem  28147  nocvxmin  28148  axcontlem4  29552  ocsh  31892  ococss  31902  shorth  31904  spansnss2  32184  h1datomi  32190  pjss2i  32289  pjssmii  32290  pjorthcoi  32778  pj3si  32816  ssrelf  33258  dfimafnf  33279  funimass4f  33280  mptssALT  33317  1stpreima  33349  2ndpreima  33350  ordtconnlem1  34604  bnj518  35564  nummin  35776  tz9.1regs  35860  cvmlift2lem1  36155  satffunlem2lem1  36257  satfvel  36265  dfon2lem6  36644  limsucncmpi  37327  finxpreclem4  38424  poimirlem3  38648  poimirlem29  38674  poimirlem32  38677  ismtyres  38849  ispridlc  39111  iss2  39383  paddss1  40981  paddss2  40982  lspindp5  42934  sn-sup2  43662  sn-sup3d  43663  dffltz  43777  pw2f1ocnv  44151  onsupmaxb  44348  naddwordnexlem2  44507  ss2iundf  44766  iunrelexp0  44809  gneispace0nelrn3  45249  nzss  45408  onfrALTlem3  45634  onfrALTlem2  45636  sspwtr  45910  sspwtrALT  45911  sspwtrALT2  45912  pwtrVD  45913  pwtrrVD  45914  suctrALT2VD  45925  suctrALT2  45926  onfrALTlem3VD  45976  onfrALTlem2VD  45978  relpmin  46049  relpfrlem  46050  ssclaxsep  46079  omssaxinf2  46085  iinssf  46260  qndenserrnopnlem  47414  dfaimafn  48342  sprsymrelfolem2  48682  mgmplusfreseq  49369  gsumlsscl  49599  lincfsuppcl  49632  linccl  49633  onsetrec  50983