Theorem ssel 3940

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 3931	. 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 3914

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 3931

This theorem is referenced by:  ssel2  3941  sseli  3942  sseld  3945  sstr2OLD  3954  nelss  4012  ssrexf  4013  ssralvOLD  4019  ssrexvOLD  4020  ralssOLD  4023  rexssOLD  4024  ssconb  4105  sscon  4106  ssdif  4107  unss1  4148  ssrin  4205  difin2  4264  reuss2  4289  reupick  4292  elpwunsn  4648  sssn  4790  uniss  4879  ss2iun  4974  ssiun  5010  iinss  5020  disjss2  5077  disjss1  5080  pwnss  5307  sspwb  5409  ssopab2bw  5507  ssopab2b  5509  pwssun  5530  xpss12  5653  frinxp  5721  ssrel  5745  ssrelOLD  5746  ssrel2  5748  ssrelrel  5759  dmss  5866  elreldm  5899  dmcosseq  5940  dmcosseqOLD  5941  relssres  5993  iss  6006  resopab2  6007  imadifssran  6124  ssrnres  6151  dfco2a  6219  cores  6222  oneqmini  6385  sucssel  6429  onssneli  6450  onssnel2i  6451  funssres  6560  fununi  6591  dfimafn  6923  funimass4  6925  funimass3  7026  dff3  7072  dff4  7073  funfvima2  7205  funfvima3  7210  f1elima  7238  isomin  7312  isofrlem  7315  riotass2  7374  ssoprab2b  7458  eqoprab2bw  7459  resoprab2  7508  ssorduni  7755  onint  7766  oninton  7771  ssnlim  7862  mptcnfimad  7965  releldm2  8022  orderseqlem  8136  dmtpos  8217  onfununi  8310  tz7.48lem  8409  tz7.49  8413  omeulem1  8546  omeulem2  8547  omsmolem  8621  omsmo  8622  ss2ixp  8883  boxriin  8913  unblem1  9239  unblem3  9241  fiint  9277  fiintOLD  9278  inf3lem2  9582  cantnflem2  9643  tcel  9698  tz9.13  9744  rankr1ag  9755  rankpwi  9776  rankelb  9777  bndrank  9794  cardlim  9925  carduni  9934  acni2  9999  dfac12r  10100  cfub  10202  cflim2  10216  fin1a2lem9  10361  axdc3lem2  10404  axdclem2  10473  gch2  10628  eltsk2g  10704  suplem1pr  11005  negn0  11607  negf1o  11608  negfi  12132  lbreu  12133  lbinf  12136  sup2  12139  sup3  12140  infm3  12142  infregelb  12167  uzwo  12870  eqreznegel  12893  xrsupsslem  13267  xrinfmsslem  13268  supxrpnf  13278  supxrunb1  13279  supxrunb2  13280  iccsupr  13403  ssnn0fi  13950  incexclem  15802  fprodmodd  15963  sumeven  16357  sumodd  16358  gcdcllem1  16469  lcmfnnval  16594  lcmfnncl  16599  dvdslcmf  16601  lcmfunsnlem2lem2  16609  lcmfdvdsb  16613  lubel  18473  clatleglb  18477  smndex1mgm  18834  smndex1sgrp  18835  smndex1mnd  18837  mulgpropd  19048  sylow2a  19549  efgi2  19655  ellspsn6  20900  rnglidlmcl  21126  submabas  22465  pmatcollpw3lem  22670  elcls2  22961  isclo2  22975  cmpsublem  23286  cmpsub  23287  hauscmplem  23293  1stcelcls  23348  llyss  23366  nllyss  23367  txkgen  23539  nrmr0reg  23636  uffix  23808  ufinffr  23816  ufilen  23817  fmfnfmlem2  23842  alexsubALTlem2  23935  alexsubALT  23938  metrest  24412  iccntr  24710  reconnlem2  24716  clmneg1  24982  clmvscom  24990  caubl  25208  dvply2g  26192  ulmss  26306  nofv  27569  nocvxminlem  27689  nocvxmin  27690  axcontlem4  28894  ocsh  31212  ococss  31222  shorth  31224  spansnss2  31504  h1datomi  31510  pjss2i  31609  pjssmii  31610  pjorthcoi  32098  pj3si  32136  ssrelf  32543  dfimafnf  32560  funimass4f  32561  mptssALT  32599  1stpreima  32630  2ndpreima  32631  indpi1  32783  isprmidlc  33418  ordtconnlem1  33914  bnj518  34876  nummin  35081  cvmlift2lem1  35289  satffunlem2lem1  35391  satfvel  35399  dfon2lem6  35776  limsucncmpi  36433  finxpreclem4  37382  poimirlem3  37617  poimirlem29  37643  poimirlem32  37646  ismtyres  37802  ispridlc  38064  iss2  38326  paddss1  39811  paddss2  39812  lspindp5  41764  sn-sup2  42479  sn-sup3d  42480  dffltz  42622  pw2f1ocnv  43026  onsupmaxb  43228  naddwordnexlem2  43387  ss2iundf  43648  iunrelexp0  43691  gneispace0nelrn3  44131  nzss  44306  onfrALTlem3  44534  onfrALTlem2  44536  sspwtr  44810  sspwtrALT  44811  sspwtrALT2  44812  pwtrVD  44813  pwtrrVD  44814  suctrALT2VD  44825  suctrALT2  44826  onfrALTlem3VD  44876  onfrALTlem2VD  44878  relpmin  44942  relpfrlem  44943  ssclaxsep  44972  omssaxinf2  44978  iinssf  45132  qndenserrnopnlem  46295  dfaimafn  47163  sprsymrelfolem2  47491  mgmplusfreseq  48150  gsumlsscl  48365  lincfsuppcl  48399  linccl  48400  onsetrec  49694