Theorem ssel 3940

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ssel2  3942  sseli  3943  sseld  3946  sstr2  3954  nelss  4012  ssrexf  4013  ssralv  4015  ssrexv  4016  ralss  4019  rexss  4020  ssconb  4102  sscon  4103  ssdif  4104  unss1  4144  ssrin  4198  difin2  4256  reuss2  4280  reupick  4283  elpwunsn  4649  sssn  4791  uniss  4878  ss2iun  4977  ssiun  5011  iinss  5021  disjss2  5078  disjss1  5081  pwnss  5311  sspwb  5411  ssopab2bw  5509  ssopab2b  5511  pwssun  5533  xpss12  5653  frinxp  5719  ssrel  5743  ssrelOLD  5744  ssrel2  5746  ssrelrel  5757  dmss  5863  elreldm  5895  dmcosseq  5933  relssres  5983  iss  5994  resopab2  5995  ssrnres  6135  dfco2a  6203  cores  6206  oneqmini  6374  sucssel  6417  onssneli  6438  onssnel2i  6439  funssres  6550  fununi  6581  dfimafn  6910  funimass4  6912  funimass3  7009  dff3  7055  dff4  7056  funfvima2  7186  funfvima3  7191  f1elima  7215  isomin  7287  isofrlem  7290  riotass2  7349  ssoprab2b  7431  eqoprab2bw  7432  resoprab2  7480  ssorduni  7718  onint  7730  oninton  7735  ssnlim  7827  releldm2  7980  orderseqlem  8094  dmtpos  8174  wfrlem10OLD  8269  onfununi  8292  tz7.48lem  8392  tz7.49  8396  omeulem1  8534  omeulem2  8535  omsmolem  8608  omsmo  8609  ss2ixp  8855  boxriin  8885  onomeneqOLD  9180  unblem1  9246  unblem3  9248  fiint  9275  inf3lem2  9574  cantnflem2  9635  tcel  9690  tz9.13  9736  rankr1ag  9747  rankpwi  9768  rankelb  9769  bndrank  9786  cardlim  9917  carduni  9926  acni2  9991  dfac12r  10091  cfub  10194  cflim2  10208  fin1a2lem9  10353  axdc3lem2  10396  axdclem2  10465  gch2  10620  eltsk2g  10696  suplem1pr  10997  negn0  11593  negf1o  11594  negfi  12113  lbreu  12114  lbinf  12117  sup2  12120  sup3  12121  infm3  12123  infregelb  12148  uzwo  12845  eqreznegel  12868  xrsupsslem  13236  xrinfmsslem  13237  supxrpnf  13247  supxrunb1  13248  supxrunb2  13249  iccsupr  13369  ssnn0fi  13900  incexclem  15732  fprodmodd  15891  sumeven  16280  sumodd  16281  gcdcllem1  16390  lcmfnnval  16511  lcmfnncl  16516  dvdslcmf  16518  lcmfunsnlem2lem2  16526  lcmfdvdsb  16530  lubel  18417  clatleglb  18421  smndex1mgm  18731  smndex1sgrp  18732  smndex1mnd  18734  mulgpropd  18932  sylow2a  19415  efgi2  19521  lspsnel6  20512  submabas  21964  pmatcollpw3lem  22169  elcls2  22462  isclo2  22476  cmpsublem  22787  cmpsub  22788  hauscmplem  22794  1stcelcls  22849  llyss  22867  nllyss  22868  txkgen  23040  nrmr0reg  23137  uffix  23309  ufinffr  23317  ufilen  23318  fmfnfmlem2  23343  alexsubALTlem2  23436  alexsubALT  23439  metrest  23917  iccntr  24221  reconnlem2  24227  clmneg1  24482  clmvscom  24490  caubl  24709  ulmss  25793  nofv  27042  nocvxminlem  27160  nocvxmin  27161  axcontlem4  27979  ocsh  30288  ococss  30298  shorth  30300  spansnss2  30580  h1datomi  30586  pjss2i  30685  pjssmii  30686  pjorthcoi  31174  pj3si  31212  ssrelf  31601  dfimafnf  31617  funimass4f  31618  mptssALT  31658  1stpreima  31688  2ndpreima  31689  isprmidlc  32296  ordtconnlem1  32594  indpi1  32708  bnj518  33587  nummin  33784  cvmlift2lem1  33983  satffunlem2lem1  34085  satfvel  34093  dfon2lem6  34449  limsucncmpi  34993  finxpreclem4  35938  poimirlem3  36154  poimirlem29  36180  poimirlem32  36183  ismtyres  36340  ispridlc  36602  iss2  36878  paddss1  38353  paddss2  38354  lspindp5  40306  sn-sup2  40996  dffltz  41030  pw2f1ocnv  41419  onsupmaxb  41631  naddwordnexlem2  41792  ss2iundf  42053  iunrelexp0  42096  gneispace0nelrn3  42536  nzss  42719  onfrALTlem3  42948  onfrALTlem2  42950  sspwtr  43225  sspwtrALT  43226  sspwtrALT2  43227  pwtrVD  43228  pwtrrVD  43229  suctrALT2VD  43240  suctrALT2  43241  onfrALTlem3VD  43291  onfrALTlem2VD  43293  iinssf  43470  qndenserrnopnlem  44658  dfaimafn  45517  sprsymrelfolem2  45805  mgmplusfreseq  46187  gsumlsscl  46579  lincfsuppcl  46614  linccl  46615  onsetrec  47273