Theorem ssel 3939

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2219. (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 3930	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 623	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1859	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2845	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2845	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  ssel2  3940  sseli  3941  sseld  3944  nelss  4011  ssrexf  4012  ralssOLD  4020  rexssOLD  4021  rabss2  4039  ssconb  4104  sscon  4105  ssdif  4106  unss1  4146  ssrin  4202  difin2  4262  reuss2  4287  reupick  4290  elpwunsn  4655  sssn  4796  uniss  4884  ss2iun  4979  ssiun  5015  iinss  5025  disjss2  5083  disjss1  5086  pwnss  5323  sspwb  5431  ssopab2bw  5533  ssopab2b  5535  pwssun  5554  xpss12  5677  frinxp  5745  ssrel  5770  ssrel2  5772  ssrelrel  5783  dmss  5893  elreldm  5926  dmcosseq  5969  dmcosseqOLD  5970  relssres  6022  iss  6038  resopab2  6039  ssrnres  6177  imadifssran  6203  imadifssranOLD  6204  dfco2a  6248  cores  6251  oneqmini  6415  sucssel  6459  onssneli  6479  onssnel2i  6480  funssres  6581  fununi  6612  dfimafn  6944  funimass4  6946  funimass3  7050  dff3  7096  dff4  7097  funfvima2  7230  funfvima3  7235  f1elima  7262  isomin  7336  isofrlem  7339  riotass2  7398  ssoprab2b  7480  eqoprab2bw  7481  resoprab2  7530  ssorduni  7777  onint  7788  oninton  7793  ssnlim  7881  mptcnfimad  7982  releldm2  8039  orderseqlem  8152  dmtpos  8233  onfununi  8327  tz7.48lem  8427  tz7.49  8431  omeulem1  8566  omeulem2  8567  omsmolem  8642  omsmo  8643  ss2ixp  8907  boxriin  8937  unblem1  9251  unblem3  9253  fiint  9285  inf3lem2  9597  cantnflem2  9658  tcel  9711  tz9.13  9762  rankr1ag  9773  rankpwi  9794  rankelb  9795  bndrank  9812  cardlim  9957  carduni  9966  acni2  10029  dfac12r  10129  cfub  10231  cflim2  10246  fin1a2lem9  10391  axdc3lem2  10434  axdclem2  10503  gch2  10659  eltsk2g  10735  suplem1pr  11036  negn0  11642  negf1o  11643  negfi  12163  lbreu  12164  lbinf  12167  sup2  12170  sup3  12171  infm3  12173  infregelb  12198  indpi1  12231  uzwo  12934  eqreznegel  12957  xrsupsslem  13332  xrinfmsslem  13333  supxrpnf  13343  supxrunb1  13344  supxrunb2  13345  iccsupr  13468  ssnn0fi  14020  incexclem  15889  fprodmodd  16050  sumeven  16444  sumodd  16445  gcdcllem1  16556  lcmfnnval  16681  lcmfnncl  16686  dvdslcmf  16688  lcmfunsnlem2lem2  16696  lcmfdvdsb  16700  lubel  18569  clatleglb  18573  smndex1mgm  18968  smndex1sgrp  18969  smndex1mnd  18971  mulgpropd  19181  sylow2a  19688  efgi2  19794  ellspsn6  21092  rnglidlmcl  21318  lidlunin0  21338  unichnlidl  21339  isprmidlc  21442  submabas  22703  pmatcollpw3lem  22908  elcls2  23199  isclo2  23213  cmpsublem  23524  cmpsub  23525  hauscmplem  23531  1stcelcls  23586  llyss  23604  nllyss  23605  txkgen  23777  nrmr0reg  23874  uffix  24046  ufinffr  24054  ufilen  24055  fmfnfmlem2  24080  alexsubALTlem2  24173  alexsubALT  24176  metrest  24649  iccntr  24947  reconnlem2  24953  clmneg1  25209  clmvscom  25217  caubl  25435  dvply2g  26414  ulmss  26525  nofv  27786  nocvxminlem  27912  nocvxmin  27913  axcontlem4  29257  ocsh  31575  ococss  31585  shorth  31587  spansnss2  31867  h1datomi  31873  pjss2i  31972  pjssmii  31973  pjorthcoi  32461  pj3si  32499  ssrelf  32900  dfimafnf  32921  funimass4f  32922  mptssALT  32959  1stpreima  32992  2ndpreima  32993  ordtconnlem1  34258  bnj518  35218  fissorduni  35422  nummin  35426  tz9.1regs  35469  cvmlift2lem1  35692  satffunlem2lem1  35794  satfvel  35802  dfon2lem6  36176  limsucncmpi  36844  finxpreclem4  37927  poimirlem3  38161  poimirlem29  38187  poimirlem32  38190  ismtyres  38346  ispridlc  38608  iss2  38882  paddss1  40480  paddss2  40481  lspindp5  42433  sn-sup2  43154  sn-sup3d  43155  dffltz  43257  pw2f1ocnv  43655  onsupmaxb  43857  naddwordnexlem2  44016  ss2iundf  44276  iunrelexp0  44319  gneispace0nelrn3  44759  nzss  44918  onfrALTlem3  45144  onfrALTlem2  45146  sspwtr  45420  sspwtrALT  45421  sspwtrALT2  45422  pwtrVD  45423  pwtrrVD  45424  suctrALT2VD  45435  suctrALT2  45436  onfrALTlem3VD  45486  onfrALTlem2VD  45488  relpmin  45552  relpfrlem  45553  ssclaxsep  45582  omssaxinf2  45588  iinssf  45747  qndenserrnopnlem  46902  dfaimafn  47790  sprsymrelfolem2  48130  mgmplusfreseq  48818  gsumlsscl  49044  lincfsuppcl  49077  linccl  49078  onsetrec  50370