Theorem ssel 3923

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-ss 3914

This theorem is referenced by:  ssel2  3924  sseli  3925  sseld  3928  sstr2OLD  3937  nelss  3995  ssrexf  3996  ssralvOLD  4002  ssrexvOLD  4003  ralssOLD  4006  rexssOLD  4007  rabss2  4024  ssconb  4089  sscon  4090  ssdif  4091  unss1  4132  ssrin  4189  difin2  4248  reuss2  4273  reupick  4276  elpwunsn  4634  sssn  4775  uniss  4864  ss2iun  4958  ssiun  4993  iinss  5003  disjss2  5059  disjss1  5062  pwnss  5288  sspwb  5388  ssopab2bw  5485  ssopab2b  5487  pwssun  5506  xpss12  5629  frinxp  5697  ssrel  5722  ssrel2  5724  ssrelrel  5735  dmss  5841  elreldm  5874  dmcosseq  5916  dmcosseqOLD  5917  dmcosseqOLDOLD  5918  relssres  5970  iss  5983  resopab2  5984  imadifssran  6098  ssrnres  6125  dfco2a  6193  cores  6196  oneqmini  6359  sucssel  6403  onssneli  6423  onssnel2i  6424  funssres  6525  fununi  6556  dfimafn  6884  funimass4  6886  funimass3  6987  dff3  7033  dff4  7034  funfvima2  7165  funfvima3  7170  f1elima  7197  isomin  7271  isofrlem  7274  riotass2  7333  ssoprab2b  7415  eqoprab2bw  7416  resoprab2  7465  ssorduni  7712  onint  7723  oninton  7728  ssnlim  7816  mptcnfimad  7918  releldm2  7975  orderseqlem  8087  dmtpos  8168  onfununi  8261  tz7.48lem  8360  tz7.49  8364  omeulem1  8497  omeulem2  8498  omsmolem  8572  omsmo  8573  ss2ixp  8834  boxriin  8864  unblem1  9176  unblem3  9178  fiint  9211  inf3lem2  9519  cantnflem2  9580  tcel  9633  tz9.13  9684  rankr1ag  9695  rankpwi  9716  rankelb  9717  bndrank  9734  cardlim  9865  carduni  9874  acni2  9937  dfac12r  10038  cfub  10140  cflim2  10154  fin1a2lem9  10299  axdc3lem2  10342  axdclem2  10411  gch2  10566  eltsk2g  10642  suplem1pr  10943  negn0  11546  negf1o  11547  negfi  12071  lbreu  12072  lbinf  12075  sup2  12078  sup3  12079  infm3  12081  infregelb  12106  uzwo  12809  eqreznegel  12832  xrsupsslem  13206  xrinfmsslem  13207  supxrpnf  13217  supxrunb1  13218  supxrunb2  13219  iccsupr  13342  ssnn0fi  13892  incexclem  15743  fprodmodd  15904  sumeven  16298  sumodd  16299  gcdcllem1  16410  lcmfnnval  16535  lcmfnncl  16540  dvdslcmf  16542  lcmfunsnlem2lem2  16550  lcmfdvdsb  16554  lubel  18420  clatleglb  18424  smndex1mgm  18815  smndex1sgrp  18816  smndex1mnd  18818  mulgpropd  19029  sylow2a  19531  efgi2  19637  ellspsn6  20927  rnglidlmcl  21153  submabas  22493  pmatcollpw3lem  22698  elcls2  22989  isclo2  23003  cmpsublem  23314  cmpsub  23315  hauscmplem  23321  1stcelcls  23376  llyss  23394  nllyss  23395  txkgen  23567  nrmr0reg  23664  uffix  23836  ufinffr  23844  ufilen  23845  fmfnfmlem2  23870  alexsubALTlem2  23963  alexsubALT  23966  metrest  24439  iccntr  24737  reconnlem2  24743  clmneg1  25009  clmvscom  25017  caubl  25235  dvply2g  26219  ulmss  26333  nofv  27596  nocvxminlem  27717  nocvxmin  27718  axcontlem4  28945  ocsh  31263  ococss  31273  shorth  31275  spansnss2  31555  h1datomi  31561  pjss2i  31660  pjssmii  31661  pjorthcoi  32149  pj3si  32187  ssrelf  32598  dfimafnf  32618  funimass4f  32619  mptssALT  32657  1stpreima  32688  2ndpreima  32689  indpi1  32841  isprmidlc  33412  ordtconnlem1  33937  bnj518  34898  fissorduni  35101  nummin  35104  tz9.1regs  35130  cvmlift2lem1  35346  satffunlem2lem1  35448  satfvel  35456  dfon2lem6  35830  limsucncmpi  36487  finxpreclem4  37436  poimirlem3  37671  poimirlem29  37697  poimirlem32  37700  ismtyres  37856  ispridlc  38118  iss2  38380  paddss1  39864  paddss2  39865  lspindp5  41817  sn-sup2  42532  sn-sup3d  42533  dffltz  42675  pw2f1ocnv  43078  onsupmaxb  43280  naddwordnexlem2  43439  ss2iundf  43700  iunrelexp0  43743  gneispace0nelrn3  44183  nzss  44358  onfrALTlem3  44585  onfrALTlem2  44587  sspwtr  44861  sspwtrALT  44862  sspwtrALT2  44863  pwtrVD  44864  pwtrrVD  44865  suctrALT2VD  44876  suctrALT2  44877  onfrALTlem3VD  44927  onfrALTlem2VD  44929  relpmin  44993  relpfrlem  44994  ssclaxsep  45023  omssaxinf2  45029  iinssf  45183  qndenserrnopnlem  46343  dfaimafn  47204  sprsymrelfolem2  47532  mgmplusfreseq  48204  gsumlsscl  48419  lincfsuppcl  48453  linccl  48454  onsetrec  49748