Theorem ssel 3989

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1776   ∈ wcel 2106   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-ss 3980

This theorem is referenced by:  ssel2  3990  sseli  3991  sseld  3994  sstr2OLD  4003  nelss  4061  ssrexf  4062  ssralvOLD  4068  ssrexvOLD  4069  ralss  4070  rexss  4071  ssconb  4152  sscon  4153  ssdif  4154  unss1  4195  ssrin  4250  difin2  4307  reuss2  4332  reupick  4335  elpwunsn  4689  sssn  4831  uniss  4920  ss2iun  5015  ssiun  5051  iinss  5061  disjss2  5118  disjss1  5121  pwnss  5358  sspwb  5460  ssopab2bw  5557  ssopab2b  5559  pwssun  5580  xpss12  5704  frinxp  5771  ssrel  5795  ssrelOLD  5796  ssrel2  5798  ssrelrel  5809  dmss  5916  elreldm  5949  dmcosseq  5990  dmcosseqOLD  5991  relssres  6042  iss  6055  resopab2  6056  ssrnres  6200  dfco2a  6268  cores  6271  oneqmini  6438  sucssel  6481  onssneli  6502  onssnel2i  6503  funssres  6612  fununi  6643  dfimafn  6971  funimass4  6973  funimass3  7074  dff3  7120  dff4  7121  funfvima2  7251  funfvima3  7256  f1elima  7283  isomin  7357  isofrlem  7360  riotass2  7418  ssoprab2b  7502  eqoprab2bw  7503  resoprab2  7552  ssorduni  7798  onint  7810  oninton  7815  ssnlim  7907  mptcnfimad  8010  releldm2  8067  orderseqlem  8181  dmtpos  8262  wfrlem10OLD  8357  onfununi  8380  tz7.48lem  8480  tz7.49  8484  omeulem1  8619  omeulem2  8620  omsmolem  8694  omsmo  8695  ss2ixp  8949  boxriin  8979  onomeneqOLD  9264  unblem1  9326  unblem3  9328  fiint  9364  fiintOLD  9365  inf3lem2  9667  cantnflem2  9728  tcel  9783  tz9.13  9829  rankr1ag  9840  rankpwi  9861  rankelb  9862  bndrank  9879  cardlim  10010  carduni  10019  acni2  10084  dfac12r  10185  cfub  10287  cflim2  10301  fin1a2lem9  10446  axdc3lem2  10489  axdclem2  10558  gch2  10713  eltsk2g  10789  suplem1pr  11090  negn0  11690  negf1o  11691  negfi  12215  lbreu  12216  lbinf  12219  sup2  12222  sup3  12223  infm3  12225  infregelb  12250  uzwo  12951  eqreznegel  12974  xrsupsslem  13346  xrinfmsslem  13347  supxrpnf  13357  supxrunb1  13358  supxrunb2  13359  iccsupr  13479  ssnn0fi  14023  incexclem  15869  fprodmodd  16030  sumeven  16421  sumodd  16422  gcdcllem1  16533  lcmfnnval  16658  lcmfnncl  16663  dvdslcmf  16665  lcmfunsnlem2lem2  16673  lcmfdvdsb  16677  lubel  18572  clatleglb  18576  smndex1mgm  18933  smndex1sgrp  18934  smndex1mnd  18936  mulgpropd  19147  sylow2a  19652  efgi2  19758  ellspsn6  21010  rnglidlmcl  21244  submabas  22600  pmatcollpw3lem  22805  elcls2  23098  isclo2  23112  cmpsublem  23423  cmpsub  23424  hauscmplem  23430  1stcelcls  23485  llyss  23503  nllyss  23504  txkgen  23676  nrmr0reg  23773  uffix  23945  ufinffr  23953  ufilen  23954  fmfnfmlem2  23979  alexsubALTlem2  24072  alexsubALT  24075  metrest  24553  iccntr  24857  reconnlem2  24863  clmneg1  25129  clmvscom  25137  caubl  25356  dvply2g  26341  ulmss  26455  nofv  27717  nocvxminlem  27837  nocvxmin  27838  axcontlem4  28997  ocsh  31312  ococss  31322  shorth  31324  spansnss2  31604  h1datomi  31610  pjss2i  31709  pjssmii  31710  pjorthcoi  32198  pj3si  32236  ssrelf  32635  dfimafnf  32653  funimass4f  32654  mptssALT  32692  1stpreima  32722  2ndpreima  32723  isprmidlc  33455  ordtconnlem1  33885  indpi1  34001  bnj518  34879  nummin  35084  cvmlift2lem1  35287  satffunlem2lem1  35389  satfvel  35397  dfon2lem6  35770  limsucncmpi  36428  finxpreclem4  37377  poimirlem3  37610  poimirlem29  37636  poimirlem32  37639  ismtyres  37795  ispridlc  38057  iss2  38326  paddss1  39800  paddss2  39801  lspindp5  41753  sn-sup2  42478  sn-sup3d  42479  dffltz  42621  pw2f1ocnv  43026  onsupmaxb  43228  naddwordnexlem2  43388  ss2iundf  43649  iunrelexp0  43692  gneispace0nelrn3  44132  nzss  44313  onfrALTlem3  44542  onfrALTlem2  44544  sspwtr  44819  sspwtrALT  44820  sspwtrALT2  44821  pwtrVD  44822  pwtrrVD  44823  suctrALT2VD  44834  suctrALT2  44835  onfrALTlem3VD  44885  onfrALTlem2VD  44887  ssclaxsep  44947  iinssf  45078  qndenserrnopnlem  46253  dfaimafn  47115  sprsymrelfolem2  47418  mgmplusfreseq  48009  gsumlsscl  48225  lincfsuppcl  48259  linccl  48260  onsetrec  48939