Theorem ssel 3925

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916

This theorem is used by:  ssel2  3926  sseli  3927  sseld  3930  nelss  3997  ssrexf  3998  ralssOLD  4006  rexssOLD  4007  rabss2  4025  ssconb  4089  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  difin2  4247  reuss2  4272  reupick  4275  elpwunsn  4645  sssn  4787  uniss  4875  ss2iun  4970  ssiun  5005  iinss  5015  disjss2  5073  disjss1  5076  pwnss  5313  sspwb  5417  ssopab2bw  5522  ssopab2b  5524  pwssun  5543  xpss12  5666  frinxp  5734  ssrel  5759  ssrel2  5761  ssrelrel  5772  dmss  5884  elreldm  5917  dmcosseq  5960  dmcosseqOLD  5961  relssres  6011  iss  6027  resopab2  6028  dfrn7  6066  ssrnres  6170  imadifssranOLD  6201  imadifssranOLDOLD  6202  dfco2a  6246  cores  6249  oneqmini  6415  sucssel  6459  onssneli  6479  onssnel2i  6480  funssres  6582  fununi  6613  dfimafn  6945  funimass4  6947  funimass3  7051  dff3  7098  dff4  7099  funfvima2  7235  funfvima3  7240  f1elima  7265  isomin  7343  isofrlem  7346  riotass2  7405  ssoprab2b  7487  eqoprab2bw  7488  resoprab2  7537  ssorduni  7791  onint  7802  oninton  7807  ssnlim  7895  mptcnfimad  7996  releldm2  8052  orderseqlem  8167  dmtpos  8248  onfununi  8342  tz7.48lemOLD  8444  tz7.49  8448  omeulem1  8583  omeulem2  8584  omsmolem  8659  omsmo  8660  ss2ixp  8931  boxriin  8961  fissorduni  9275  unblem1  9277  unblem3  9279  fiint  9311  inf3lem2  9623  cantnflem2  9684  tcel  9737  tz9.13  9791  rankr1ag  9803  rankpwi  9825  rankelb  9826  bndrank  9847  cardlim  10046  carduni  10055  acni2  10118  dfac12r  10218  cfub  10319  cflim2  10334  fin1a2lem9  10479  axdc3lem2  10522  axdclem2  10591  gch2  10753  eltsk2g  10829  suplem1pr  11130  negn0  11738  negf1o  11739  negfi  12259  lbreu  12260  lbinf  12263  sup2  12266  sup3  12267  infm3  12269  infregelb  12294  indpi1  12327  uzwo  13031  eqreznegel  13054  xrsupsslem  13430  xrinfmsslem  13431  supxrpnf  13441  supxrunb1  13442  supxrunb2  13443  iccsupr  13566  ssnn0fi  14121  incexclem  15998  fprodmodd  16157  sumeven  16550  sumodd  16551  gcdcllem1  16662  lcmfnnval  16792  lcmfnncl  16797  dvdslcmf  16799  lcmfunsnlem2lem2  16807  lcmfdvdsb  16811  lubel  18681  clatleglb  18685  smndex1mgm  19099  smndex1sgrp  19100  smndex1mnd  19102  mulgpropd  19319  sylow2a  19826  efgi2  19932  ellspsn6  21262  rnglidlmcl  21488  lidlunin0  21508  unichnlidl  21509  isprmidlc  21621  submabas  22886  pmatcollpw3lem  23094  elcls2  23385  isclo2  23399  cmpsublem  23710  cmpsub  23711  hauscmplem  23717  1stcelcls  23773  llyss  23791  nllyss  23792  txkgen  23964  nrmr0reg  24061  uffix  24233  ufinffr  24241  ufilen  24242  fmfnfmlem2  24267  alexsubALTlem2  24360  alexsubALT  24363  metrest  24836  iccntr  25134  reconnlem2  25140  clmneg1  25396  clmvscom  25404  caubl  25622  dvply2g  26599  ulmss  26717  nofv  28007  nocvxminlem  28133  nocvxmin  28134  axcontlem4  29538  ocsh  31878  ococss  31888  shorth  31890  spansnss2  32170  h1datomi  32176  pjss2i  32275  pjssmii  32276  pjorthcoi  32764  pj3si  32802  ssrelf  33202  dfimafnf  33223  funimass4f  33224  mptssALT  33261  1stpreima  33293  2ndpreima  33294  ordtconnlem1  34549  bnj518  35509  nummin  35711  tz9.1regs  35785  cvmlift2lem1  36046  satffunlem2lem1  36148  satfvel  36156  dfon2lem6  36530  limsucncmpi  37213  finxpreclem4  38297  poimirlem3  38521  poimirlem29  38547  poimirlem32  38550  ismtyres  38722  ispridlc  38984  iss2  39256  paddss1  40854  paddss2  40855  lspindp5  42807  sn-sup2  43535  sn-sup3d  43536  dffltz  43650  pw2f1ocnv  44023  onsupmaxb  44225  naddwordnexlem2  44384  ss2iundf  44644  iunrelexp0  44687  gneispace0nelrn3  45127  nzss  45286  onfrALTlem3  45512  onfrALTlem2  45514  sspwtr  45788  sspwtrALT  45789  sspwtrALT2  45790  pwtrVD  45791  pwtrrVD  45792  suctrALT2VD  45803  suctrALT2  45804  onfrALTlem3VD  45854  onfrALTlem2VD  45856  relpmin  45920  relpfrlem  45921  ssclaxsep  45950  omssaxinf2  45956  iinssf  46122  qndenserrnopnlem  47276  dfaimafn  48204  sprsymrelfolem2  48544  mgmplusfreseq  49231  gsumlsscl  49461  lincfsuppcl  49494  linccl  49495  onsetrec  50770