Theorem sseq2d 3970

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 3964	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseq12d  3971  sseqtrd  3974  sbcrel  5769  funimass2  6621  fnssresb  6659  fnimaeq0  6670  foimacnv  6840  fvelimab  6955  ssimaexg  6969  ralima  7237  knatar  7357  frecseq123  8280  frrlem4  8287  onfununi  8329  oaordi  8532  oawordeulem  8540  oaass  8547  odi  8565  omass  8566  oen0  8573  oelim2  8582  nnaordi  8605  nnawordex  8624  naddunif  8681  pssnn  9154  fissuni  9315  dffi3  9392  cantnfle  9641  cantnflem1  9659  trcl  9698  r1sdom  9747  scottelrankd  9874  iscard2  9963  alephordi  10059  alephgeom  10067  cardaleph  10074  cardalephex  10075  ackbij2lem4  10225  cflm  10234  cfslbn  10252  cofsmo  10254  cfsmolem  10255  cfcoflem  10257  coftr  10258  alephsing  10261  fin23lem28  10325  fin23lem30  10327  fin23lem33  10330  fin1a2lem9  10393  axdc3lem2  10436  ttukeylem5  10498  pwfseqlem4a  10647  pwfseqlem4  10648  wunex2  10724  inar1  10761  sstskm  10828  fsuppmapnn0fiubex  14030  swrdnd  14694  swrd0  14698  repswswrd  14823  rtrclreclem1  15096  rtrclreclem2  15098  summolem2  15769  summo  15770  zsum  15771  sumz  15775  sumss  15777  fsumcvg3  15782  prodmolem2  15991  prodmo  15992  zprod  15993  prod1  16000  vdwlem1  17042  vdwlem12  17053  vdwlem13  17054  ramub2  17075  rami  17076  ramz2  17085  setsstruct2  17235  prdsval  17509  pwsle  17547  mrcuni  17678  gsumpropd  18737  gsumpropd2lem  18738  gsumress  18741  eqgfval  19245  sscntz  19397  resscntz  19404  lsmlub  19735  efgrelexlemb  19821  efgcpbllemb  19826  gsumval3a  19974  gsumzaddlem  19992  gsumzoppg  20015  dmdprd  20071  dprdcntz  20081  subgdmdprd  20107  subrngpropd  20654  subrgpropd  20694  islss  21036  lsslss  21063  lsspropd  21119  lsmelpr  21193  lbspropd  21201  lsslinds  21962  ltbval  22175  opsrval  22178  mhpval  22283  isbasisg  23085  tgval  23093  tgss3  23124  restbas  23296  tgrest  23297  restcld  23310  restopn2  23315  restntr  23320  cnpnei  23402  cncls2  23411  perfcls  23503  cmpsublem  23537  cmpsub  23538  cmpcld  23540  uncmp  23541  hauscmplem  23544  cmpfi  23546  nconnsubb  23561  clsconn  23568  hausllycmp  23632  1stckgenlem  23691  txbas  23705  ptbasfi  23719  txcnpi  23746  ptcnp  23760  txcmplem1  23779  txcmplem2  23780  xkococnlem  23797  qtopcld  23851  fbasssin  23974  fbssint  23976  fbun  23978  fbasrn  24022  filufint  24058  ufinffr  24067  ufildr  24069  ustval  24341  trust  24367  elmopn  24580  neibl  24639  cfilucfil  24697  icccmplem1  24961  icccmplem2  24962  bndth  25098  isphtpc  25134  metcld  25446  bcthlem1  25464  bcth  25469  ovolfioo  25607  ovolficc  25608  elovolmr  25616  ovoliunlem3  25644  ovolicc2  25662  volsuplem  25695  dyadmax  25738  dyadmbllem  25739  dyadmbl  25740  precsexlem6  28383  precsexlem7  28384  bdayfinbndlem1  28638  bdayfinbndlem2  28639  lnssplng  29052  incistruhgr  29407  edgssv2  29526  wksfval  29937  2wlkdlem9  30261  3wlkdlem9  30497  sspval  31053  ubth  31203  orthin  31776  chssoc  31826  chsscon3  31830  chsscon1  31831  h1datom  31912  pjoml6i  31919  osum  31975  spansncv  31983  pjcjt2  32022  pjopyth  32050  hstel2  32549  hstle  32560  stj  32565  dmdbr5  32638  mdslmd1lem1  32655  atord  32718  chirredlem4  32723  atcvat4i  32727  mdsymlem2  32734  mdsymlem3  32735  mdsymlem8  32740  padct  33041  ssnnssfz  33110  pwrssmgc  33298  lindspropd  33674  idlsrgval  33771  constr01  34110  constrmon  34112  constrextdg2lem  34116  constrextdg2  34117  constrfiss  34119  tpr2rico  34280  ordtrestNEW  34289  sigaval  34479  issiga  34480  issgon  34491  oms0  34665  omssubadd  34668  elscottrankss  35494  subgrwlk  35602  umgr2cycllem  35610  kur14  35686  cvmliftlem15  35768  satfsschain  35834  mclsrcl  36031  mclsval  36033  nmulprop  36660  ivthALT  36824  isfne  36828  topfne  36843  neibastop3  36851  tailfb  36866  filnetlem1  36867  filnetlem4  36870  relowlssretop  37987  rdgssun  38002  poimirlem24  38273  mblfinlem2  38287  sstotbnd2  38403  sstotbnd  38404  sstotbnd3  38405  ssbnd  38417  cntotbnd  38425  cnpwstotbnd  38426  ismtyres  38437  heibor1lem  38438  heiborlem1  38440  heiborlem6  38445  heiborlem8  38447  exidreslem  38506  scottexf  38795  scott0f  38796  cnvref4  38977  dfrefrels2  39220  dfrefrel2  39222  lshpcmp  39740  lsmsat  39760  lsmsatcv  39762  lfl1dim  39873  lfl1dim2N  39874  lkrss2N  39921  psubspset  40496  paddss  40597  psubclsetN  40688  dilfsetN  40904  dilsetN  40905  diaglbN  41807  dibglbN  41918  dihlspsnat  42085  dihglb2  42094  dochffval  42101  dochfval  42102  dochvalr  42109  dochord2N  42123  dochsncom  42134  dihjat1lem  42180  dvh4dimat  42190  dvh3dimatN  42191  dvh2dimatN  42192  dochexmidlem1  42212  lpolsetN  42234  lpolconN  42239  hdmaplkr  42665  hdmapoc  42683  hlhillcs  42710  ismrc  43412  incssnn0  43422  nacsfix  43423  hbt  43837  oacl2g  44037  omcl2  44040  ofoaf  44062  naddwordnexlem4  44108  ss2iundf  44365  clsk1indlem1  44751  clsk1independent  44752  isotone1  44754  isotone2  44755  ntrclsiso  44773  ntrclsk2  44774  ssinc  45785  uzfissfz  46022  stoweidlem50  46744  stoweidlem57  46751  fourierdlem20  46821  fourierdlem50  46850  fourierdlem64  46864  fourierdlem86  46886  fourierdlem103  46903  fourierdlem104  46904  ovnval  47235  hoicvrrex  47250  ovnlecvr  47252  ovncvrrp  47258  ovnsubaddlem1  47264  hoidmvlelem3  47291  hoidmvle  47294  ovnhoilem1  47295  ovnhoi  47297  ovnlecvr2  47304  ovncvr2  47305  hspmbl  47323  ovolval4lem2  47344  ovolval5lem2  47347  ovolval5lem3  47348  ovolval5  47349  ovnovollem1  47350  ovnovollem2  47351  sprsymrelfvlem  48216  grlimedgclnbgr  48737  grlimgrtri  48745  grilcbri2  48753  uspgrsprf  48888  uspgrsprfo  48890  ssnn0ssfz  49106  lincfsuppcl  49170  iunlub  49576  lubeldm2d  49713  glbeldm2d  49714