Theorem ssel 3957

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2810  df-ss 3948

This theorem is referenced by:  ssel2  3958  sseli  3959  sseld  3962  sstr2OLD  3971  nelss  4029  ssrexf  4030  ssralvOLD  4036  ssrexvOLD  4037  ralssOLD  4040  rexssOLD  4041  ssconb  4122  sscon  4123  ssdif  4124  unss1  4165  ssrin  4222  difin2  4281  reuss2  4306  reupick  4309  elpwunsn  4665  sssn  4807  uniss  4896  ss2iun  4991  ssiun  5027  iinss  5037  disjss2  5094  disjss1  5097  pwnss  5327  sspwb  5429  ssopab2bw  5527  ssopab2b  5529  pwssun  5550  xpss12  5674  frinxp  5742  ssrel  5766  ssrelOLD  5767  ssrel2  5769  ssrelrel  5780  dmss  5887  elreldm  5920  dmcosseq  5961  dmcosseqOLD  5962  relssres  6014  iss  6027  resopab2  6028  imadifssran  6145  ssrnres  6172  dfco2a  6240  cores  6243  oneqmini  6410  sucssel  6454  onssneli  6475  onssnel2i  6476  funssres  6585  fununi  6616  dfimafn  6946  funimass4  6948  funimass3  7049  dff3  7095  dff4  7096  funfvima2  7228  funfvima3  7233  f1elima  7261  isomin  7335  isofrlem  7338  riotass2  7397  ssoprab2b  7481  eqoprab2bw  7482  resoprab2  7531  ssorduni  7778  onint  7789  oninton  7794  ssnlim  7886  mptcnfimad  7990  releldm2  8047  orderseqlem  8161  dmtpos  8242  wfrlem10OLD  8337  onfununi  8360  tz7.48lem  8460  tz7.49  8464  omeulem1  8599  omeulem2  8600  omsmolem  8674  omsmo  8675  ss2ixp  8929  boxriin  8959  onomeneqOLD  9243  unblem1  9305  unblem3  9307  fiint  9343  fiintOLD  9344  inf3lem2  9648  cantnflem2  9709  tcel  9764  tz9.13  9810  rankr1ag  9821  rankpwi  9842  rankelb  9843  bndrank  9860  cardlim  9991  carduni  10000  acni2  10065  dfac12r  10166  cfub  10268  cflim2  10282  fin1a2lem9  10427  axdc3lem2  10470  axdclem2  10539  gch2  10694  eltsk2g  10770  suplem1pr  11071  negn0  11671  negf1o  11672  negfi  12196  lbreu  12197  lbinf  12200  sup2  12203  sup3  12204  infm3  12206  infregelb  12231  uzwo  12932  eqreznegel  12955  xrsupsslem  13328  xrinfmsslem  13329  supxrpnf  13339  supxrunb1  13340  supxrunb2  13341  iccsupr  13464  ssnn0fi  14008  incexclem  15857  fprodmodd  16018  sumeven  16411  sumodd  16412  gcdcllem1  16523  lcmfnnval  16648  lcmfnncl  16653  dvdslcmf  16655  lcmfunsnlem2lem2  16663  lcmfdvdsb  16667  lubel  18529  clatleglb  18533  smndex1mgm  18890  smndex1sgrp  18891  smndex1mnd  18893  mulgpropd  19104  sylow2a  19605  efgi2  19711  ellspsn6  20956  rnglidlmcl  21182  submabas  22521  pmatcollpw3lem  22726  elcls2  23017  isclo2  23031  cmpsublem  23342  cmpsub  23343  hauscmplem  23349  1stcelcls  23404  llyss  23422  nllyss  23423  txkgen  23595  nrmr0reg  23692  uffix  23864  ufinffr  23872  ufilen  23873  fmfnfmlem2  23898  alexsubALTlem2  23991  alexsubALT  23994  metrest  24468  iccntr  24766  reconnlem2  24772  clmneg1  25038  clmvscom  25046  caubl  25265  dvply2g  26249  ulmss  26363  nofv  27626  nocvxminlem  27746  nocvxmin  27747  axcontlem4  28951  ocsh  31269  ococss  31279  shorth  31281  spansnss2  31561  h1datomi  31567  pjss2i  31666  pjssmii  31667  pjorthcoi  32155  pj3si  32193  ssrelf  32600  dfimafnf  32619  funimass4f  32620  mptssALT  32658  1stpreima  32689  2ndpreima  32690  indpi1  32842  isprmidlc  33467  ordtconnlem1  33960  bnj518  34922  nummin  35127  cvmlift2lem1  35329  satffunlem2lem1  35431  satfvel  35439  dfon2lem6  35811  limsucncmpi  36468  finxpreclem4  37417  poimirlem3  37652  poimirlem29  37678  poimirlem32  37681  ismtyres  37837  ispridlc  38099  iss2  38367  paddss1  39841  paddss2  39842  lspindp5  41794  sn-sup2  42489  sn-sup3d  42490  dffltz  42632  pw2f1ocnv  43036  onsupmaxb  43238  naddwordnexlem2  43397  ss2iundf  43658  iunrelexp0  43701  gneispace0nelrn3  44141  nzss  44316  onfrALTlem3  44544  onfrALTlem2  44546  sspwtr  44820  sspwtrALT  44821  sspwtrALT2  44822  pwtrVD  44823  pwtrrVD  44824  suctrALT2VD  44835  suctrALT2  44836  onfrALTlem3VD  44886  onfrALTlem2VD  44888  relpmin  44952  relpfrlem  44953  ssclaxsep  44982  omssaxinf2  44988  iinssf  45142  qndenserrnopnlem  46306  dfaimafn  47174  sprsymrelfolem2  47487  mgmplusfreseq  48120  gsumlsscl  48335  lincfsuppcl  48369  linccl  48370  onsetrec  49552