Theorem ssel 3822

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ssel	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem ssel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3816	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	biimpi 208	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3	2	19.21bi 2232	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	3	anim2d 607	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	eximdv 2018	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) → ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2822	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2822	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3imtr4g 288	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 386  ∀wal 1656   = wceq 1658  ∃wex 1880   ∈ wcel 2166   ⊆ wss 3799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-in 3806  df-ss 3813

This theorem is referenced by:  ssel2  3823  sseli  3824  sseld  3827  sstr2  3835  nelss  3890  ssrexf  3891  ssralv  3892  ssrexv  3893  ralss  3894  rexss  3895  ssconb  3971  sscon  3972  ssdif  3973  unss1  4010  ssrin  4063  difin2  4120  reuss2  4137  reupick  4141  elpwunsn  4445  sssn  4576  uniss  4682  ss2iun  4757  ssiun  4783  iinss  4792  disjss2  4845  disjss1  4848  pwnss  5053  sspwb  5139  ssopab2b  5229  pwssun  5247  soss  5282  xpss12  5358  frinxp  5420  ssrel  5443  ssrel2  5445  ssrelrel  5455  dmss  5556  elreldm  5583  dmcosseq  5621  relssres  5675  iss  5685  resopab2  5686  idrefOLD  5752  ssrnres  5814  dfco2a  5877  cores  5880  oneqmini  6015  sucssel  6056  onssneli  6073  onssnel2i  6074  funssres  6167  fununi  6198  dfimafn  6493  funimass4  6495  funimass3  6583  dff3  6622  dff4  6623  funfvima2  6750  funfvima3  6752  f1elima  6776  isomin  6843  isofrlem  6846  riotass2  6894  ssoprab2b  6973  resoprab2  7018  ssorduni  7247  onint  7257  oninton  7262  ssnlim  7345  releldm2  7481  reldmtpos  7626  dmtpos  7630  wfrlem10  7691  onfununi  7705  tz7.48lem  7803  tz7.49  7807  omeulem1  7930  omeulem2  7931  omsmolem  8001  omsmo  8002  ss2ixp  8189  boxriin  8218  onomeneq  8420  unblem1  8482  unblem3  8484  fiint  8507  inf3lem2  8804  cantnflem2  8865  tcel  8899  tz9.13  8932  rankr1ag  8943  rankpwi  8964  rankelb  8965  bndrank  8982  cardlim  9112  carduni  9121  acni2  9183  dfac12r  9284  cfub  9387  cflim2  9401  fin1a2lem9  9546  axdc3lem2  9589  axdclem2  9658  gch2  9813  eltsk2g  9889  suplem1pr  10190  negn0  10784  negf1o  10785  fimaxre  11299  negfi  11302  fiminre  11303  lbreu  11304  lbinf  11307  sup2  11310  sup3  11311  infm3  11313  infregelb  11338  uzwo  12035  eqreznegel  12058  xrsupsslem  12426  xrinfmsslem  12427  supxrpnf  12437  supxrunb1  12438  supxrunb2  12439  iccsupr  12556  ssnn0fi  13080  incexclem  14943  fprodmodd  15101  sumeven  15485  sumodd  15486  gcdcllem1  15595  lcmfnnval  15711  lcmfnncl  15716  dvdslcmf  15718  lcmfunsnlem2lem2  15726  lcmfdvdsb  15730  lubel  17476  clatleglb  17480  mulgpropd  17936  sylow2a  18386  efgi2  18490  lspsnel6  19354  submabas  20753  pmatcollpw3lem  20959  elcls2  21250  isclo2  21264  cmpsublem  21574  cmpsub  21575  hauscmplem  21581  1stcelcls  21636  llyss  21654  nllyss  21655  txkgen  21827  nrmr0reg  21924  uffix  22096  ufinffr  22104  ufilen  22105  fmfnfmlem2  22130  alexsubALTlem2  22223  alexsubALT  22226  metrest  22700  iccntr  22995  reconnlem2  23001  clmneg1  23252  clmvscom  23260  caubl  23477  ulmss  24551  axcontlem4  26267  ocsh  28698  ococss  28708  shorth  28710  spansnss2  28990  h1datomi  28996  pjss2i  29095  pjssmii  29096  pjorthcoi  29584  pj3si  29622  ssrelf  29975  dfimafnf  29986  funimass4f  29987  mptssALT  30023  1stpreima  30033  2ndpreima  30034  ordtconnlem1  30516  indpi1  30628  bnj518  31503  cvmlift2lem1  31831  dfon2lem6  32232  trpredmintr  32270  orderseqlem  32292  frrlem5b  32325  frrlem5d  32327  nofv  32350  nocvxminlem  32433  nocvxmin  32434  limsucncmpi  32978  finxpreclem4  33777  poimirlem3  33957  poimirlem29  33983  poimirlem32  33986  ismtyres  34150  ispridlc  34412  iss2  34661  paddss1  35893  paddss2  35894  lspindp5  37846  dffltz  38098  pw2f1ocnv  38448  ss2iundf  38793  iunrelexp0  38836  gneispace0nelrn3  39281  nzss  39357  onfrALTlem3  39589  onfrALTlem2  39591  sspwtr  39876  sspwtrALT  39877  sspwtrALT2  39878  pwtrVD  39879  pwtrrVD  39880  suctrALT2VD  39891  suctrALT2  39892  onfrALTlem3VD  39942  onfrALTlem2VD  39944  iinssf  40140  qndenserrnopnlem  41309  dfaimafn  42068  sprsymrelfolem2  42591  mgmplusfreseq  42621  gsumlsscl  43012  lincfsuppcl  43050  linccl  43051  onsetrec  43350