Theorem ssel 4002

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 3993	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 22	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 611	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1830	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2820	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2820	. . 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 1777   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  ssel2  4003  sseli  4004  sseld  4007  sstr2OLD  4016  nelss  4074  ssrexf  4075  ssralvOLD  4081  ssrexvOLD  4082  ralss  4083  rexss  4084  ssconb  4165  sscon  4166  ssdif  4167  unss1  4208  ssrin  4263  difin2  4320  reuss2  4345  reupick  4348  elpwunsn  4707  sssn  4851  uniss  4939  ss2iun  5033  ssiun  5069  iinss  5079  disjss2  5136  disjss1  5139  pwnss  5370  sspwb  5469  ssopab2bw  5566  ssopab2b  5568  pwssun  5590  xpss12  5715  frinxp  5782  ssrel  5806  ssrelOLD  5807  ssrel2  5809  ssrelrel  5820  dmss  5927  elreldm  5960  dmcosseq  5999  dmcosseqOLD  6000  relssres  6051  iss  6064  resopab2  6065  ssrnres  6209  dfco2a  6277  cores  6280  oneqmini  6447  sucssel  6490  onssneli  6511  onssnel2i  6512  funssres  6622  fununi  6653  dfimafn  6984  funimass4  6986  funimass3  7087  dff3  7134  dff4  7135  funfvima2  7268  funfvima3  7273  f1elima  7300  isomin  7373  isofrlem  7376  riotass2  7435  ssoprab2b  7519  eqoprab2bw  7520  resoprab2  7569  ssorduni  7814  onint  7826  oninton  7831  ssnlim  7923  mptcnfimad  8027  releldm2  8084  orderseqlem  8198  dmtpos  8279  wfrlem10OLD  8374  onfununi  8397  tz7.48lem  8497  tz7.49  8501  omeulem1  8638  omeulem2  8639  omsmolem  8713  omsmo  8714  ss2ixp  8968  boxriin  8998  onomeneqOLD  9292  unblem1  9356  unblem3  9358  fiint  9394  fiintOLD  9395  inf3lem2  9698  cantnflem2  9759  tcel  9814  tz9.13  9860  rankr1ag  9871  rankpwi  9892  rankelb  9893  bndrank  9910  cardlim  10041  carduni  10050  acni2  10115  dfac12r  10216  cfub  10318  cflim2  10332  fin1a2lem9  10477  axdc3lem2  10520  axdclem2  10589  gch2  10744  eltsk2g  10820  suplem1pr  11121  negn0  11719  negf1o  11720  negfi  12244  lbreu  12245  lbinf  12248  sup2  12251  sup3  12252  infm3  12254  infregelb  12279  uzwo  12976  eqreznegel  12999  xrsupsslem  13369  xrinfmsslem  13370  supxrpnf  13380  supxrunb1  13381  supxrunb2  13382  iccsupr  13502  ssnn0fi  14036  incexclem  15884  fprodmodd  16045  sumeven  16435  sumodd  16436  gcdcllem1  16545  lcmfnnval  16671  lcmfnncl  16676  dvdslcmf  16678  lcmfunsnlem2lem2  16686  lcmfdvdsb  16690  lubel  18584  clatleglb  18588  smndex1mgm  18942  smndex1sgrp  18943  smndex1mnd  18945  mulgpropd  19156  sylow2a  19661  efgi2  19767  ellspsn6  21015  rnglidlmcl  21249  submabas  22605  pmatcollpw3lem  22810  elcls2  23103  isclo2  23117  cmpsublem  23428  cmpsub  23429  hauscmplem  23435  1stcelcls  23490  llyss  23508  nllyss  23509  txkgen  23681  nrmr0reg  23778  uffix  23950  ufinffr  23958  ufilen  23959  fmfnfmlem2  23984  alexsubALTlem2  24077  alexsubALT  24080  metrest  24558  iccntr  24862  reconnlem2  24868  clmneg1  25134  clmvscom  25142  caubl  25361  dvply2g  26344  ulmss  26458  nofv  27720  nocvxminlem  27840  nocvxmin  27841  axcontlem4  29000  ocsh  31315  ococss  31325  shorth  31327  spansnss2  31607  h1datomi  31613  pjss2i  31712  pjssmii  31713  pjorthcoi  32201  pj3si  32239  ssrelf  32637  dfimafnf  32655  funimass4f  32656  mptssALT  32693  1stpreima  32718  2ndpreima  32719  isprmidlc  33440  ordtconnlem1  33870  indpi1  33984  bnj518  34862  nummin  35067  cvmlift2lem1  35270  satffunlem2lem1  35372  satfvel  35380  dfon2lem6  35752  limsucncmpi  36411  finxpreclem4  37360  poimirlem3  37583  poimirlem29  37609  poimirlem32  37612  ismtyres  37768  ispridlc  38030  iss2  38300  paddss1  39774  paddss2  39775  lspindp5  41727  sn-sup2  42447  sn-sup3d  42448  dffltz  42589  pw2f1ocnv  42994  onsupmaxb  43200  naddwordnexlem2  43360  ss2iundf  43621  iunrelexp0  43664  gneispace0nelrn3  44104  nzss  44286  onfrALTlem3  44515  onfrALTlem2  44517  sspwtr  44792  sspwtrALT  44793  sspwtrALT2  44794  pwtrVD  44795  pwtrrVD  44796  suctrALT2VD  44807  suctrALT2  44808  onfrALTlem3VD  44858  onfrALTlem2VD  44860  iinssf  45040  qndenserrnopnlem  46218  dfaimafn  47080  sprsymrelfolem2  47367  mgmplusfreseq  47888  gsumlsscl  48108  lincfsuppcl  48142  linccl  48143  onsetrec  48800