Theorem ssel 3937

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 3928	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 612	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1832	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2804	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2804	. . 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 3911

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 2803  df-ss 3928

This theorem is referenced by:  ssel2  3938  sseli  3939  sseld  3942  sstr2OLD  3951  nelss  4009  ssrexf  4010  ssralvOLD  4016  ssrexvOLD  4017  ralssOLD  4020  rexssOLD  4021  ssconb  4101  sscon  4102  ssdif  4103  unss1  4144  ssrin  4201  difin2  4260  reuss2  4285  reupick  4288  elpwunsn  4644  sssn  4786  uniss  4875  ss2iun  4970  ssiun  5005  iinss  5015  disjss2  5072  disjss1  5075  pwnss  5302  sspwb  5404  ssopab2bw  5502  ssopab2b  5504  pwssun  5523  xpss12  5646  frinxp  5714  ssrel  5737  ssrel2  5739  ssrelrel  5750  dmss  5856  elreldm  5888  dmcosseq  5929  dmcosseqOLD  5930  relssres  5982  iss  5995  resopab2  5996  imadifssran  6112  ssrnres  6139  dfco2a  6207  cores  6210  oneqmini  6373  sucssel  6417  onssneli  6438  onssnel2i  6439  funssres  6544  fununi  6575  dfimafn  6905  funimass4  6907  funimass3  7008  dff3  7054  dff4  7055  funfvima2  7187  funfvima3  7192  f1elima  7220  isomin  7294  isofrlem  7297  riotass2  7356  ssoprab2b  7438  eqoprab2bw  7439  resoprab2  7488  ssorduni  7735  onint  7746  oninton  7751  ssnlim  7842  mptcnfimad  7944  releldm2  8001  orderseqlem  8113  dmtpos  8194  onfununi  8287  tz7.48lem  8386  tz7.49  8390  omeulem1  8523  omeulem2  8524  omsmolem  8598  omsmo  8599  ss2ixp  8860  boxriin  8890  unblem1  9215  unblem3  9217  fiint  9253  fiintOLD  9254  inf3lem2  9558  cantnflem2  9619  tcel  9674  tz9.13  9720  rankr1ag  9731  rankpwi  9752  rankelb  9753  bndrank  9770  cardlim  9901  carduni  9910  acni2  9975  dfac12r  10076  cfub  10178  cflim2  10192  fin1a2lem9  10337  axdc3lem2  10380  axdclem2  10449  gch2  10604  eltsk2g  10680  suplem1pr  10981  negn0  11583  negf1o  11584  negfi  12108  lbreu  12109  lbinf  12112  sup2  12115  sup3  12116  infm3  12118  infregelb  12143  uzwo  12846  eqreznegel  12869  xrsupsslem  13243  xrinfmsslem  13244  supxrpnf  13254  supxrunb1  13255  supxrunb2  13256  iccsupr  13379  ssnn0fi  13926  incexclem  15778  fprodmodd  15939  sumeven  16333  sumodd  16334  gcdcllem1  16445  lcmfnnval  16570  lcmfnncl  16575  dvdslcmf  16577  lcmfunsnlem2lem2  16585  lcmfdvdsb  16589  lubel  18449  clatleglb  18453  smndex1mgm  18810  smndex1sgrp  18811  smndex1mnd  18813  mulgpropd  19024  sylow2a  19525  efgi2  19631  ellspsn6  20876  rnglidlmcl  21102  submabas  22441  pmatcollpw3lem  22646  elcls2  22937  isclo2  22951  cmpsublem  23262  cmpsub  23263  hauscmplem  23269  1stcelcls  23324  llyss  23342  nllyss  23343  txkgen  23515  nrmr0reg  23612  uffix  23784  ufinffr  23792  ufilen  23793  fmfnfmlem2  23818  alexsubALTlem2  23911  alexsubALT  23914  metrest  24388  iccntr  24686  reconnlem2  24692  clmneg1  24958  clmvscom  24966  caubl  25184  dvply2g  26168  ulmss  26282  nofv  27545  nocvxminlem  27665  nocvxmin  27666  axcontlem4  28870  ocsh  31185  ococss  31195  shorth  31197  spansnss2  31477  h1datomi  31483  pjss2i  31582  pjssmii  31583  pjorthcoi  32071  pj3si  32109  ssrelf  32516  dfimafnf  32533  funimass4f  32534  mptssALT  32572  1stpreima  32603  2ndpreima  32604  indpi1  32756  isprmidlc  33391  ordtconnlem1  33887  bnj518  34849  nummin  35054  cvmlift2lem1  35262  satffunlem2lem1  35364  satfvel  35372  dfon2lem6  35749  limsucncmpi  36406  finxpreclem4  37355  poimirlem3  37590  poimirlem29  37616  poimirlem32  37619  ismtyres  37775  ispridlc  38037  iss2  38299  paddss1  39784  paddss2  39785  lspindp5  41737  sn-sup2  42452  sn-sup3d  42453  dffltz  42595  pw2f1ocnv  42999  onsupmaxb  43201  naddwordnexlem2  43360  ss2iundf  43621  iunrelexp0  43664  gneispace0nelrn3  44104  nzss  44279  onfrALTlem3  44507  onfrALTlem2  44509  sspwtr  44783  sspwtrALT  44784  sspwtrALT2  44785  pwtrVD  44786  pwtrrVD  44787  suctrALT2VD  44798  suctrALT2  44799  onfrALTlem3VD  44849  onfrALTlem2VD  44851  relpmin  44915  relpfrlem  44916  ssclaxsep  44945  omssaxinf2  44951  iinssf  45105  qndenserrnopnlem  46268  dfaimafn  47139  sprsymrelfolem2  47467  mgmplusfreseq  48126  gsumlsscl  48341  lincfsuppcl  48375  linccl  48376  onsetrec  49670