Theorem ssel 3925

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2213. (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 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		id 23	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	anim2d 624	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
4	3	aleximi 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5		dfclel 2837	. . 3 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
6		dfclel 2837	. . 3 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
7	4, 5, 6	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
8	1, 7	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916

This theorem is used by:  ssel2  3926  sseli  3927  sseld  3930  nelss  3997  ssrexf  3998  ralssOLD  4006  rexssOLD  4007  rabss2  4025  ssconb  4089  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  difin2  4247  reuss2  4272  reupick  4275  elpwunsn  4645  sssn  4787  uniss  4875  ss2iun  4970  ssiun  5005  iinss  5015  disjss2  5073  disjss1  5076  pwnss  5313  sspwb  5417  ssopab2bw  5522  ssopab2b  5524  pwssun  5543  xpss12  5666  frinxp  5734  ssrel  5759  ssrel2  5761  ssrelrel  5772  dmss  5884  elreldm  5917  dmcosseq  5960  dmcosseqOLD  5961  relssres  6011  iss  6027  resopab2  6028  dfrn7  6066  ssrnres  6170  imadifssranOLD  6202  imadifssranOLDOLD  6203  dfco2a  6247  cores  6250  oneqmini  6416  sucssel  6460  onssneli  6480  onssnel2i  6481  funssres  6584  fununi  6615  dfimafn  6947  funimass4  6949  funimass3  7053  dff3  7100  dff4  7101  funfvima2  7237  funfvima3  7242  f1elima  7267  isomin  7345  isofrlem  7348  riotass2  7407  ssoprab2b  7489  eqoprab2bw  7490  resoprab2  7539  ssorduni  7793  onint  7804  oninton  7809  ssnlim  7897  mptcnfimad  7998  releldm2  8054  orderseqlem  8174  dmtpos  8255  onfununi  8349  tz7.48lemOLD  8451  tz7.49  8455  omeulem1  8590  omeulem2  8591  omsmolem  8666  omsmo  8667  ss2ixp  8938  boxriin  8968  fissorduni  9282  unblem1  9284  unblem3  9286  fiint  9318  inf3lem2  9630  cantnflem2  9691  tcel  9744  tz9.13  9798  rankr1ag  9810  rankpwi  9832  rankelb  9833  bndrank  9854  cardlim  10053  carduni  10062  acni2  10125  dfac12r  10225  cfub  10326  cflim2  10341  fin1a2lem9  10486  axdc3lem2  10529  axdclem2  10598  gch2  10760  eltsk2g  10836  suplem1pr  11137  negn0  11745  negf1o  11746  negfi  12266  lbreu  12267  lbinf  12270  sup2  12273  sup3  12274  infm3  12276  infregelb  12301  indpi1  12334  uzwo  13038  eqreznegel  13061  xrsupsslem  13437  xrinfmsslem  13438  supxrpnf  13448  supxrunb1  13449  supxrunb2  13450  iccsupr  13573  ssnn0fi  14128  incexclem  16005  fprodmodd  16164  sumeven  16557  sumodd  16558  gcdcllem1  16669  lcmfnnval  16799  lcmfnncl  16804  dvdslcmf  16806  lcmfunsnlem2lem2  16814  lcmfdvdsb  16818  lubel  18688  clatleglb  18692  smndex1mgm  19106  smndex1sgrp  19107  smndex1mnd  19109  mulgpropd  19326  sylow2a  19833  efgi2  19939  ellspsn6  21269  rnglidlmcl  21495  lidlunin0  21515  unichnlidl  21516  isprmidlc  21628  submabas  22893  pmatcollpw3lem  23101  elcls2  23392  isclo2  23406  cmpsublem  23717  cmpsub  23718  hauscmplem  23724  1stcelcls  23780  llyss  23798  nllyss  23799  txkgen  23971  nrmr0reg  24068  uffix  24240  ufinffr  24248  ufilen  24249  fmfnfmlem2  24274  alexsubALTlem2  24367  alexsubALT  24370  metrest  24843  iccntr  25141  reconnlem2  25147  clmneg1  25403  clmvscom  25411  caubl  25629  dvply2g  26606  ulmss  26724  nofv  28014  nocvxminlem  28140  nocvxmin  28141  axcontlem4  29545  ocsh  31885  ococss  31895  shorth  31897  spansnss2  32177  h1datomi  32183  pjss2i  32282  pjssmii  32283  pjorthcoi  32771  pj3si  32809  ssrelf  33209  dfimafnf  33230  funimass4f  33231  mptssALT  33268  1stpreima  33300  2ndpreima  33301  ordtconnlem1  34556  bnj518  35516  nummin  35722  tz9.1regs  35802  cvmlift2lem1  36067  satffunlem2lem1  36169  satfvel  36177  dfon2lem6  36550  limsucncmpi  37233  finxpreclem4  38318  poimirlem3  38542  poimirlem29  38568  poimirlem32  38571  ismtyres  38743  ispridlc  39005  iss2  39277  paddss1  40875  paddss2  40876  lspindp5  42828  sn-sup2  43556  sn-sup3d  43557  dffltz  43671  pw2f1ocnv  44044  onsupmaxb  44241  naddwordnexlem2  44400  ss2iundf  44659  iunrelexp0  44702  gneispace0nelrn3  45142  nzss  45301  onfrALTlem3  45527  onfrALTlem2  45529  sspwtr  45803  sspwtrALT  45804  sspwtrALT2  45805  pwtrVD  45806  pwtrrVD  45807  suctrALT2VD  45818  suctrALT2  45819  onfrALTlem3VD  45869  onfrALTlem2VD  45871  relpmin  45942  relpfrlem  45943  ssclaxsep  45972  omssaxinf2  45978  iinssf  46153  qndenserrnopnlem  47307  dfaimafn  48235  sprsymrelfolem2  48575  mgmplusfreseq  49262  gsumlsscl  49492  lincfsuppcl  49525  linccl  49526  onsetrec  50801