Theorem ssel 3925

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2213. (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 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 624	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1865	. . 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 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

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

This theorem is used by:  ssel2  3926  sseli  3927  sseld  3930  nelss  3997  ssrexf  3998  ralssOLD  4006  rexssOLD  4007  rabss2  4025  ssconb  4089  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  difin2  4247  reuss2  4272  reupick  4275  elpwunsn  4645  sssn  4787  uniss  4875  ss2iun  4970  ssiun  5005  iinss  5015  disjss2  5073  disjss1  5076  pwnss  5316  sspwb  5424  ssopab2bw  5526  ssopab2b  5528  pwssun  5547  xpss12  5670  frinxp  5738  ssrel  5763  ssrel2  5765  ssrelrel  5776  dmss  5886  elreldm  5919  dmcosseq  5962  dmcosseqOLD  5963  relssres  6015  iss  6031  resopab2  6032  ssrnres  6171  imadifssran  6197  imadifssranOLD  6198  dfco2a  6242  cores  6245  oneqmini  6411  sucssel  6455  onssneli  6475  onssnel2i  6476  funssres  6577  fununi  6608  dfimafn  6940  funimass4  6942  funimass3  7046  dff3  7093  dff4  7094  funfvima2  7230  funfvima3  7235  f1elima  7260  isomin  7338  isofrlem  7341  riotass2  7400  ssoprab2b  7482  eqoprab2bw  7483  resoprab2  7532  ssorduni  7778  onint  7789  oninton  7794  ssnlim  7882  mptcnfimad  7983  releldm2  8040  orderseqlem  8155  dmtpos  8236  onfununi  8330  tz7.48lem  8430  tz7.49  8434  omeulem1  8569  omeulem2  8570  omsmolem  8645  omsmo  8646  ss2ixp  8917  boxriin  8947  unblem1  9262  unblem3  9264  fiint  9296  inf3lem2  9608  cantnflem2  9669  tcel  9722  tz9.13  9773  rankr1ag  9784  rankpwi  9805  rankelb  9806  bndrank  9823  cardlim  9977  carduni  9986  acni2  10049  dfac12r  10149  cfub  10250  cflim2  10265  fin1a2lem9  10410  axdc3lem2  10453  axdclem2  10522  gch2  10684  eltsk2g  10760  suplem1pr  11061  negn0  11667  negf1o  11668  negfi  12188  lbreu  12189  lbinf  12192  sup2  12195  sup3  12196  infm3  12198  infregelb  12223  indpi1  12256  uzwo  12960  eqreznegel  12983  xrsupsslem  13359  xrinfmsslem  13360  supxrpnf  13370  supxrunb1  13371  supxrunb2  13372  iccsupr  13495  ssnn0fi  14049  incexclem  15925  fprodmodd  16084  sumeven  16477  sumodd  16478  gcdcllem1  16589  lcmfnnval  16714  lcmfnncl  16719  dvdslcmf  16721  lcmfunsnlem2lem2  16729  lcmfdvdsb  16733  lubel  18602  clatleglb  18606  smndex1mgm  19019  smndex1sgrp  19020  smndex1mnd  19022  mulgpropd  19239  sylow2a  19746  efgi2  19852  ellspsn6  21178  rnglidlmcl  21404  lidlunin0  21424  unichnlidl  21425  isprmidlc  21535  submabas  22800  pmatcollpw3lem  23008  elcls2  23299  isclo2  23313  cmpsublem  23624  cmpsub  23625  hauscmplem  23631  1stcelcls  23687  llyss  23705  nllyss  23706  txkgen  23878  nrmr0reg  23975  uffix  24147  ufinffr  24155  ufilen  24156  fmfnfmlem2  24181  alexsubALTlem2  24274  alexsubALT  24277  metrest  24750  iccntr  25048  reconnlem2  25054  clmneg1  25310  clmvscom  25318  caubl  25536  dvply2g  26515  ulmss  26633  nofv  27893  nocvxminlem  28019  nocvxmin  28020  axcontlem4  29424  ocsh  31764  ococss  31774  shorth  31776  spansnss2  32056  h1datomi  32062  pjss2i  32161  pjssmii  32162  pjorthcoi  32650  pj3si  32688  ssrelf  33088  dfimafnf  33109  funimass4f  33110  mptssALT  33147  1stpreima  33179  2ndpreima  33180  ordtconnlem1  34434  bnj518  35395  fissorduni  35594  nummin  35598  tz9.1regs  35660  cvmlift2lem1  35881  satffunlem2lem1  35983  satfvel  35991  dfon2lem6  36365  limsucncmpi  37064  finxpreclem4  38148  poimirlem3  38372  poimirlem29  38398  poimirlem32  38401  ismtyres  38558  ispridlc  38820  iss2  39092  paddss1  40690  paddss2  40691  lspindp5  42643  sn-sup2  43379  sn-sup3d  43380  dffltz  43480  pw2f1ocnv  43878  onsupmaxb  44080  naddwordnexlem2  44239  ss2iundf  44499  iunrelexp0  44542  gneispace0nelrn3  44982  nzss  45141  onfrALTlem3  45367  onfrALTlem2  45369  sspwtr  45643  sspwtrALT  45644  sspwtrALT2  45645  pwtrVD  45646  pwtrrVD  45647  suctrALT2VD  45658  suctrALT2  45659  onfrALTlem3VD  45709  onfrALTlem2VD  45711  relpmin  45775  relpfrlem  45776  ssclaxsep  45805  omssaxinf2  45811  iinssf  45970  qndenserrnopnlem  47125  dfaimafn  48053  sprsymrelfolem2  48393  mgmplusfreseq  49080  gsumlsscl  49310  lincfsuppcl  49343  linccl  49344  onsetrec  50634