Theorem ssel 3959

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1778   ∈ wcel 2107   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2808  df-ss 3950

This theorem is referenced by:  ssel2  3960  sseli  3961  sseld  3964  sstr2OLD  3973  nelss  4031  ssrexf  4032  ssralvOLD  4038  ssrexvOLD  4039  ralssOLD  4042  rexssOLD  4043  ssconb  4124  sscon  4125  ssdif  4126  unss1  4167  ssrin  4224  difin2  4283  reuss2  4308  reupick  4311  elpwunsn  4666  sssn  4808  uniss  4897  ss2iun  4992  ssiun  5028  iinss  5038  disjss2  5095  disjss1  5098  pwnss  5334  sspwb  5436  ssopab2bw  5534  ssopab2b  5536  pwssun  5557  xpss12  5682  frinxp  5750  ssrel  5774  ssrelOLD  5775  ssrel2  5777  ssrelrel  5788  dmss  5895  elreldm  5928  dmcosseq  5969  dmcosseqOLD  5970  relssres  6022  iss  6035  resopab2  6036  imadifssran  6153  ssrnres  6180  dfco2a  6248  cores  6251  oneqmini  6417  sucssel  6460  onssneli  6481  onssnel2i  6482  funssres  6591  fununi  6622  dfimafn  6952  funimass4  6954  funimass3  7055  dff3  7101  dff4  7102  funfvima2  7234  funfvima3  7239  f1elima  7266  isomin  7340  isofrlem  7343  riotass2  7401  ssoprab2b  7485  eqoprab2bw  7486  resoprab2  7535  ssorduni  7782  onint  7793  oninton  7798  ssnlim  7890  mptcnfimad  7994  releldm2  8051  orderseqlem  8165  dmtpos  8246  wfrlem10OLD  8341  onfununi  8364  tz7.48lem  8464  tz7.49  8468  omeulem1  8603  omeulem2  8604  omsmolem  8678  omsmo  8679  ss2ixp  8933  boxriin  8963  onomeneqOLD  9249  unblem1  9311  unblem3  9313  fiint  9349  fiintOLD  9350  inf3lem2  9652  cantnflem2  9713  tcel  9768  tz9.13  9814  rankr1ag  9825  rankpwi  9846  rankelb  9847  bndrank  9864  cardlim  9995  carduni  10004  acni2  10069  dfac12r  10170  cfub  10272  cflim2  10286  fin1a2lem9  10431  axdc3lem2  10474  axdclem2  10543  gch2  10698  eltsk2g  10774  suplem1pr  11075  negn0  11675  negf1o  11676  negfi  12200  lbreu  12201  lbinf  12204  sup2  12207  sup3  12208  infm3  12210  infregelb  12235  uzwo  12936  eqreznegel  12959  xrsupsslem  13332  xrinfmsslem  13333  supxrpnf  13343  supxrunb1  13344  supxrunb2  13345  iccsupr  13465  ssnn0fi  14009  incexclem  15855  fprodmodd  16016  sumeven  16407  sumodd  16408  gcdcllem1  16519  lcmfnnval  16644  lcmfnncl  16649  dvdslcmf  16651  lcmfunsnlem2lem2  16659  lcmfdvdsb  16663  lubel  18533  clatleglb  18537  smndex1mgm  18894  smndex1sgrp  18895  smndex1mnd  18897  mulgpropd  19108  sylow2a  19610  efgi2  19716  ellspsn6  20965  rnglidlmcl  21193  submabas  22551  pmatcollpw3lem  22756  elcls2  23047  isclo2  23061  cmpsublem  23372  cmpsub  23373  hauscmplem  23379  1stcelcls  23434  llyss  23452  nllyss  23453  txkgen  23625  nrmr0reg  23722  uffix  23894  ufinffr  23902  ufilen  23903  fmfnfmlem2  23928  alexsubALTlem2  24021  alexsubALT  24024  metrest  24500  iccntr  24798  reconnlem2  24804  clmneg1  25070  clmvscom  25078  caubl  25297  dvply2g  26281  ulmss  26395  nofv  27657  nocvxminlem  27777  nocvxmin  27778  axcontlem4  28931  ocsh  31249  ococss  31259  shorth  31261  spansnss2  31541  h1datomi  31547  pjss2i  31646  pjssmii  31647  pjorthcoi  32135  pj3si  32173  ssrelf  32574  dfimafnf  32593  funimass4f  32594  mptssALT  32632  1stpreima  32663  2ndpreima  32664  indpi1  32792  isprmidlc  33416  ordtconnlem1  33864  bnj518  34841  nummin  35046  cvmlift2lem1  35248  satffunlem2lem1  35350  satfvel  35358  dfon2lem6  35730  limsucncmpi  36387  finxpreclem4  37336  poimirlem3  37571  poimirlem29  37597  poimirlem32  37600  ismtyres  37756  ispridlc  38018  iss2  38286  paddss1  39760  paddss2  39761  lspindp5  41713  sn-sup2  42446  sn-sup3d  42447  dffltz  42589  pw2f1ocnv  42994  onsupmaxb  43196  naddwordnexlem2  43356  ss2iundf  43617  iunrelexp0  43660  gneispace0nelrn3  44100  nzss  44281  onfrALTlem3  44509  onfrALTlem2  44511  sspwtr  44786  sspwtrALT  44787  sspwtrALT2  44788  pwtrVD  44789  pwtrrVD  44790  suctrALT2VD  44801  suctrALT2  44802  onfrALTlem3VD  44852  onfrALTlem2VD  44854  relpmin  44918  relpfrlem  44919  ssclaxsep  44944  omssaxinf2  44950  iinssf  45088  qndenserrnopnlem  46257  dfaimafn  47123  sprsymrelfolem2  47426  mgmplusfreseq  48027  gsumlsscl  48242  lincfsuppcl  48276  linccl  48277  onsetrec  49223