Theorem ssel 3931

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

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3922

This theorem is referenced by:  ssel2  3932  sseli  3933  sseld  3936  nelss  4003  ssrexf  4004  ralssOLD  4012  rexssOLD  4013  rabss2  4031  ssconb  4096  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  difin2  4254  reuss2  4279  reupick  4282  elpwunsn  4650  sssn  4792  uniss  4880  ss2iun  4975  ssiun  5011  iinss  5021  disjss2  5079  disjss1  5082  pwnss  5322  sspwb  5430  ssopab2bw  5532  ssopab2b  5534  pwssun  5553  xpss12  5676  frinxp  5744  ssrel  5769  ssrel2  5771  ssrelrel  5782  dmss  5892  elreldm  5925  dmcosseq  5968  dmcosseqOLD  5969  relssres  6021  iss  6037  resopab2  6038  ssrnres  6176  imadifssran  6202  imadifssranOLD  6203  dfco2a  6247  cores  6250  oneqmini  6414  sucssel  6458  onssneli  6478  onssnel2i  6479  funssres  6580  fununi  6611  dfimafn  6943  funimass4  6945  funimass3  7049  dff3  7095  dff4  7096  funfvima2  7229  funfvima3  7234  f1elima  7261  isomin  7335  isofrlem  7338  riotass2  7397  ssoprab2b  7479  eqoprab2bw  7480  resoprab2  7529  ssorduni  7774  onint  7785  oninton  7790  ssnlim  7878  mptcnfimad  7979  releldm2  8036  orderseqlem  8149  dmtpos  8230  onfununi  8324  tz7.48lem  8424  tz7.49  8428  omeulem1  8563  omeulem2  8564  omsmolem  8639  omsmo  8640  ss2ixp  8904  boxriin  8934  unblem1  9248  unblem3  9250  fiint  9282  inf3lem2  9594  cantnflem2  9655  tcel  9708  tz9.13  9759  rankr1ag  9770  rankpwi  9791  rankelb  9792  bndrank  9809  cardlim  9954  carduni  9963  acni2  10026  dfac12r  10126  cfub  10227  cflim2  10242  fin1a2lem9  10387  axdc3lem2  10430  axdclem2  10499  gch2  10655  eltsk2g  10731  suplem1pr  11032  negn0  11638  negf1o  11639  negfi  12159  lbreu  12160  lbinf  12163  sup2  12166  sup3  12167  infm3  12169  infregelb  12194  indpi1  12227  uzwo  12930  eqreznegel  12953  xrsupsslem  13328  xrinfmsslem  13329  supxrpnf  13339  supxrunb1  13340  supxrunb2  13341  iccsupr  13464  ssnn0fi  14017  incexclem  15886  fprodmodd  16047  sumeven  16440  sumodd  16441  gcdcllem1  16552  lcmfnnval  16677  lcmfnncl  16682  dvdslcmf  16684  lcmfunsnlem2lem2  16692  lcmfdvdsb  16696  lubel  18565  clatleglb  18569  smndex1mgm  18964  smndex1sgrp  18965  smndex1mnd  18967  mulgpropd  19177  sylow2a  19684  efgi2  19790  ellspsn6  21115  rnglidlmcl  21341  lidlunin0  21361  unichnlidl  21362  isprmidlc  21472  submabas  22735  pmatcollpw3lem  22940  elcls2  23231  isclo2  23245  cmpsublem  23556  cmpsub  23557  hauscmplem  23563  1stcelcls  23618  llyss  23636  nllyss  23637  txkgen  23809  nrmr0reg  23906  uffix  24078  ufinffr  24086  ufilen  24087  fmfnfmlem2  24112  alexsubALTlem2  24205  alexsubALT  24208  metrest  24681  iccntr  24979  reconnlem2  24985  clmneg1  25241  clmvscom  25249  caubl  25467  dvply2g  26446  ulmss  26560  nofv  27821  nocvxminlem  27947  nocvxmin  27948  axcontlem4  29317  ocsh  31635  ococss  31645  shorth  31647  spansnss2  31927  h1datomi  31933  pjss2i  32032  pjssmii  32033  pjorthcoi  32521  pj3si  32559  ssrelf  32960  dfimafnf  32981  funimass4f  32982  mptssALT  33019  1stpreima  33052  2ndpreima  33053  ordtconnlem1  34314  bnj518  35274  fissorduni  35480  nummin  35484  tz9.1regs  35547  cvmlift2lem1  35794  satffunlem2lem1  35896  satfvel  35904  dfon2lem6  36278  limsucncmpi  36956  finxpreclem4  38040  poimirlem3  38274  poimirlem29  38300  poimirlem32  38303  ismtyres  38459  ispridlc  38721  iss2  38993  paddss1  40591  paddss2  40592  lspindp5  42544  sn-sup2  43265  sn-sup3d  43266  dffltz  43366  pw2f1ocnv  43764  onsupmaxb  43966  naddwordnexlem2  44125  ss2iundf  44385  iunrelexp0  44428  gneispace0nelrn3  44868  nzss  45027  onfrALTlem3  45253  onfrALTlem2  45255  sspwtr  45529  sspwtrALT  45530  sspwtrALT2  45531  pwtrVD  45532  pwtrrVD  45533  suctrALT2VD  45544  suctrALT2  45545  onfrALTlem3VD  45595  onfrALTlem2VD  45597  relpmin  45661  relpfrlem  45662  ssclaxsep  45691  omssaxinf2  45697  iinssf  45856  qndenserrnopnlem  47011  dfaimafn  47902  sprsymrelfolem2  48242  mgmplusfreseq  48930  gsumlsscl  49160  lincfsuppcl  49193  linccl  49194  onsetrec  50486