Theorem ssel 3971

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  ssel2  3973  sseli  3974  sseld  3977  sstr2  3985  nelss  4043  ssrexf  4044  ssralv  4046  ssrexv  4047  ralss  4050  rexss  4051  ssconb  4133  sscon  4134  ssdif  4135  unss1  4175  ssrin  4229  difin2  4287  reuss2  4311  reupick  4314  elpwunsn  4683  sssn  4825  uniss  4911  ss2iun  5009  ssiun  5043  iinss  5053  disjss2  5110  disjss1  5113  pwnss  5345  sspwb  5445  ssopab2bw  5543  ssopab2b  5545  pwssun  5567  xpss12  5687  frinxp  5754  ssrel  5778  ssrelOLD  5779  ssrel2  5781  ssrelrel  5792  dmss  5899  elreldm  5931  dmcosseq  5970  relssres  6020  iss  6033  resopab2  6034  ssrnres  6176  dfco2a  6244  cores  6247  oneqmini  6415  sucssel  6458  onssneli  6479  onssnel2i  6480  funssres  6591  fununi  6622  dfimafn  6955  funimass4  6957  funimass3  7057  dff3  7104  dff4  7105  funfvima2  7237  funfvima3  7242  f1elima  7267  isomin  7339  isofrlem  7342  riotass2  7401  ssoprab2b  7483  eqoprab2bw  7484  resoprab2  7533  ssorduni  7775  onint  7787  oninton  7792  ssnlim  7884  mptcnfimad  7984  releldm2  8041  orderseqlem  8156  dmtpos  8237  wfrlem10OLD  8332  onfununi  8355  tz7.48lem  8455  tz7.49  8459  omeulem1  8596  omeulem2  8597  omsmolem  8671  omsmo  8672  ss2ixp  8922  boxriin  8952  onomeneqOLD  9247  unblem1  9313  unblem3  9315  fiint  9342  inf3lem2  9646  cantnflem2  9707  tcel  9762  tz9.13  9808  rankr1ag  9819  rankpwi  9840  rankelb  9841  bndrank  9858  cardlim  9989  carduni  9998  acni2  10063  dfac12r  10163  cfub  10266  cflim2  10280  fin1a2lem9  10425  axdc3lem2  10468  axdclem2  10537  gch2  10692  eltsk2g  10768  suplem1pr  11069  negn0  11667  negf1o  11668  negfi  12187  lbreu  12188  lbinf  12191  sup2  12194  sup3  12195  infm3  12197  infregelb  12222  uzwo  12919  eqreznegel  12942  xrsupsslem  13312  xrinfmsslem  13313  supxrpnf  13323  supxrunb1  13324  supxrunb2  13325  iccsupr  13445  ssnn0fi  13976  incexclem  15808  fprodmodd  15967  sumeven  16357  sumodd  16358  gcdcllem1  16467  lcmfnnval  16588  lcmfnncl  16593  dvdslcmf  16595  lcmfunsnlem2lem2  16603  lcmfdvdsb  16607  lubel  18499  clatleglb  18503  smndex1mgm  18852  smndex1sgrp  18853  smndex1mnd  18855  mulgpropd  19064  sylow2a  19567  efgi2  19673  lspsnel6  20871  rnglidlmcl  21105  submabas  22473  pmatcollpw3lem  22678  elcls2  22971  isclo2  22985  cmpsublem  23296  cmpsub  23297  hauscmplem  23303  1stcelcls  23358  llyss  23376  nllyss  23377  txkgen  23549  nrmr0reg  23646  uffix  23818  ufinffr  23826  ufilen  23827  fmfnfmlem2  23852  alexsubALTlem2  23945  alexsubALT  23948  metrest  24426  iccntr  24730  reconnlem2  24736  clmneg1  25002  clmvscom  25010  caubl  25229  dvply2g  26212  ulmss  26326  nofv  27583  nocvxminlem  27703  nocvxmin  27704  axcontlem4  28771  ocsh  31086  ococss  31096  shorth  31098  spansnss2  31378  h1datomi  31384  pjss2i  31483  pjssmii  31484  pjorthcoi  31972  pj3si  32010  ssrelf  32398  dfimafnf  32414  funimass4f  32415  mptssALT  32454  1stpreima  32480  2ndpreima  32481  isprmidlc  33153  ordtconnlem1  33515  indpi1  33629  bnj518  34507  nummin  34704  cvmlift2lem1  34902  satffunlem2lem1  35004  satfvel  35012  dfon2lem6  35374  limsucncmpi  35919  finxpreclem4  36863  poimirlem3  37085  poimirlem29  37111  poimirlem32  37114  ismtyres  37270  ispridlc  37532  iss2  37805  paddss1  39279  paddss2  39280  lspindp5  41232  sn-sup2  41996  dffltz  42030  pw2f1ocnv  42430  onsupmaxb  42639  naddwordnexlem2  42800  ss2iundf  43061  iunrelexp0  43104  gneispace0nelrn3  43544  nzss  43726  onfrALTlem3  43955  onfrALTlem2  43957  sspwtr  44232  sspwtrALT  44233  sspwtrALT2  44234  pwtrVD  44235  pwtrrVD  44236  suctrALT2VD  44247  suctrALT2  44248  onfrALTlem3VD  44298  onfrALTlem2VD  44300  iinssf  44476  qndenserrnopnlem  45657  dfaimafn  46517  sprsymrelfolem2  46805  mgmplusfreseq  47199  gsumlsscl  47419  lincfsuppcl  47453  linccl  47454  onsetrec  48111