Theorem sseq2d 3945

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq2d	⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq2 3939	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  sseq12d  3946  sseqtrd  3949  sbcrel  5762  funimass2  6645  fnssresb  6683  fnimaeq0  6694  foimacnv  6864  fvelimab  6980  ssimaexg  6994  ralima  7266  knatar  7390  frecseq123  8328  frrlem4  8335  onfununi  8377  oaordi  8582  oawordeulem  8590  oaass  8597  odi  8615  omass  8616  oen0  8623  oelim2  8632  nnaordi  8655  nnawordex  8674  naddunif  8731  pssnn  9212  fissuni  9374  dffi3  9450  cantnfle  9699  cantnflem1  9717  trcl  9756  r1sdom  9808  scottex  9960  scottelrankd  9975  iscard2  10084  alephordi  10180  alephgeom  10188  cardaleph  10195  cardalephex  10196  ackbij2lem4  10346  cflm  10354  cfslbn  10372  cofsmo  10374  cfsmolem  10375  cfcoflem  10377  coftr  10378  alephsing  10381  fin23lem28  10445  fin23lem30  10447  fin23lem33  10450  fin1a2lem9  10513  axdc3lem2  10556  ttukeylem5  10618  pwfseqlem4a  10773  pwfseqlem4  10774  wunex2  10850  inar1  10887  sstskm  10954  fsuppmapnn0fiubex  14162  swrdnd  14832  swrd0  14836  repswswrd  14963  rtrclreclem1  15239  rtrclreclem2  15241  summolem2  15911  summo  15912  zsum  15913  sumz  15917  sumss  15919  fsumcvg3  15924  prodmolem2  16131  prodmo  16132  zprod  16133  prod1  16140  vdwlem1  17188  vdwlem12  17199  vdwlem13  17200  ramub2  17221  rami  17222  ramz2  17231  setsstruct2  17381  prdsval  17655  pwsle  17693  mrcuni  17824  gsumpropd  18896  gsumpropd2lem  18897  gsumress  18900  eqgfval  19417  sscntz  19570  resscntz  19577  lsmlub  19908  efgrelexlemb  19994  efgcpbllemb  19999  gsumval3a  20147  gsumzaddlem  20165  gsumzoppg  20188  dmdprd  20244  dprdcntz  20254  subgdmdprd  20280  subrngpropd  20850  subrgpropd  20890  islss  21239  lsslss  21266  lsspropd  21322  lsmelpr  21396  lbspropd  21404  lsslinds  22167  ltbval  22382  opsrval  22385  mhpval  22490  isbasisg  23295  tgval  23303  tgss3  23334  restbas  23506  tgrest  23507  restcld  23520  restopn2  23525  restntr  23530  cnpnei  23612  cncls2  23621  perfcls  23713  cmpsublem  23747  cmpsub  23748  cmpcld  23750  uncmp  23751  hauscmplem  23754  cmpfi  23756  nconnsubb  23771  clsconn  23778  hausllycmp  23843  1stckgenlem  23902  txbas  23916  ptbasfi  23930  txcnpi  23957  ptcnp  23971  txcmplem1  23990  txcmplem2  23991  xkococnlem  24008  qtopcld  24062  fbasssin  24185  fbssint  24187  fbun  24189  fbasrn  24233  filufint  24269  ufinffr  24278  ufildr  24280  ustval  24552  trust  24578  elmopn  24791  neibl  24850  cfilucfil  24908  icccmplem1  25172  icccmplem2  25173  bndth  25309  isphtpc  25345  metcld  25657  bcthlem1  25675  bcth  25680  ovolfioo  25818  ovolficc  25819  elovolmr  25827  ovoliunlem3  25855  ovolicc2  25873  volsuplem  25906  dyadmax  25949  dyadmbllem  25950  dyadmbl  25951  precsexlem6  28628  precsexlem7  28629  bdayfinbndlem1  28883  bdayfinbndlem2  28884  lnssplng  29300  incistruhgr  29687  edgssv2  29809  wksfval  30220  subgrwlk  30299  2wlkdlem9  30553  3wlkdlem9  30799  sspval  31355  ubth  31505  orthin  32078  chssoc  32128  chsscon3  32132  chsscon1  32133  h1datom  32214  pjoml6i  32221  osum  32277  spansncv  32285  pjcjt2  32324  pjopyth  32352  hstel2  32851  hstle  32862  stj  32867  dmdbr5  32940  mdslmd1lem1  32957  atord  33020  chirredlem4  33025  atcvat4i  33029  mdsymlem2  33036  mdsymlem3  33037  mdsymlem8  33042  padct  33381  ssnnssfz  33449  pwrssmgc  33631  lindspropd  34008  idlsrgval  34105  constr01  34444  constrmon  34446  constrextdg2lem  34450  constrextdg2  34451  constrfiss  34453  tpr2rico  34614  ordtrestNEW  34623  sigaval  34813  issiga  34814  issgon  34825  oms0  34999  omssubadd  35002  elscottrankss  35831  0elscott  35837  acwer1prclem  35851  maxssj0  36006  onprcf1acwevdlem1  36045  kur14  36148  cvmliftlem15  36230  satfsschain  36296  mclsrcl  36493  mclsval  36495  nmulprop  37117  ivthALT  37301  isfne  37305  topfne  37320  neibastop3  37328  tailfb  37343  filnetlem1  37344  filnetlem4  37347  relowlssretop  38478  rdgssun  38493  poimirlem24  38754  mblfinlem2  38768  sstotbnd2  38900  sstotbnd  38901  sstotbnd3  38902  ssbnd  38914  cntotbnd  38922  cnpwstotbnd  38923  ismtyres  38934  heibor1lem  38935  heiborlem1  38937  heiborlem6  38942  heiborlem8  38944  exidreslem  39003  scottexf  39292  scott0f  39293  cnvref4  39474  dfrefrels2  39717  dfrefrel2  39719  lshpcmp  40237  lsmsat  40257  lsmsatcv  40259  lfl1dim  40370  lfl1dim2N  40371  lkrss2N  40418  psubspset  40993  paddss  41094  psubclsetN  41185  dilfsetN  41401  dilsetN  41402  diaglbN  42304  dibglbN  42415  dihlspsnat  42582  dihglb2  42591  dochffval  42598  dochfval  42599  dochvalr  42606  dochord2N  42620  dochsncom  42631  dihjat1lem  42677  dvh4dimat  42687  dvh3dimatN  42688  dvh2dimatN  42689  dochexmidlem1  42709  lpolsetN  42731  lpolconN  42736  hdmaplkr  43162  hdmapoc  43180  hlhillcs  43207  ismrc  43905  incssnn0  43915  nacsfix  43916  hbt  44324  oacl2g  44524  omcl2  44527  ofoaf  44549  naddwordnexlem4  44595  ss2iundf  44851  clsk1indlem1  45237  clsk1independent  45238  isotone1  45240  isotone2  45241  ntrclsiso  45259  ntrclsk2  45260  ssinc  46307  uzfissfz  46543  stoweidlem50  47265  stoweidlem57  47272  fourierdlem20  47342  fourierdlem50  47371  fourierdlem64  47385  fourierdlem86  47407  fourierdlem103  47424  fourierdlem104  47425  ovnval  47756  hoicvrrex  47771  ovnlecvr  47773  ovncvrrp  47779  ovnsubaddlem1  47785  hoidmvlelem3  47812  hoidmvle  47815  ovnhoilem1  47816  ovnhoi  47818  ovnlecvr2  47825  ovncvr2  47826  hspmbl  47844  ovolval4lem2  47865  ovolval5lem2  47868  ovolval5lem3  47869  ovolval5  47870  ovnovollem1  47871  ovnovollem2  47872  sprsymrelfvlem  48777  grlimedgclnbgr  49298  grlimgrtri  49306  grilcbri2  49314  uspgrsprf  49449  uspgrsprfo  49451  ssnn0ssfz  49666  lincfsuppcl  49730  iunlub  50137  lubeldm2d  50277  glbeldm2d  50278