Theorem sseq2d 3955

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseq12d  3956  sseqtrd  3959  sbcrel  5730  funimass2  6575  fnssresb  6614  fnimaeq0  6625  foimacnv  6791  fvelimab  6906  ssimaexg  6920  ralima  7185  knatar  7305  frecseq123  8225  frrlem4  8232  onfununi  8274  oaordi  8474  oawordeulem  8482  oaass  8489  odi  8507  omass  8508  oen0  8515  oelim2  8524  nnaordi  8547  nnawordex  8566  naddunif  8622  pssnn  9096  fissuni  9260  dffi3  9337  cantnfle  9583  cantnflem1  9601  trcl  9640  r1sdom  9689  iscard2  9891  alephordi  9987  alephgeom  9995  cardaleph  10002  cardalephex  10003  ackbij2lem4  10154  cflm  10163  cfslbn  10180  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  coftr  10186  alephsing  10189  fin23lem28  10253  fin23lem30  10255  fin23lem33  10258  fin1a2lem9  10321  axdc3lem2  10364  ttukeylem5  10426  pwfseqlem4a  10575  pwfseqlem4  10576  wunex2  10652  inar1  10689  sstskm  10756  fsuppmapnn0fiubex  13945  swrdnd  14608  swrd0  14612  repswswrd  14737  rtrclreclem1  15010  rtrclreclem2  15012  summolem2  15669  summo  15670  zsum  15671  sumz  15675  sumss  15677  fsumcvg3  15682  prodmolem2  15891  prodmo  15892  zprod  15893  prod1  15900  vdwlem1  16943  vdwlem12  16954  vdwlem13  16955  ramub2  16976  rami  16977  ramz2  16986  setsstruct2  17135  prdsval  17409  pwsle  17447  mrcuni  17578  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  eqgfval  19142  sscntz  19292  resscntz  19299  lsmlub  19630  efgrelexlemb  19716  efgcpbllemb  19721  gsumval3a  19869  gsumzaddlem  19887  gsumzoppg  19910  dmdprd  19966  dprdcntz  19976  subgdmdprd  20002  subrngpropd  20536  subrgpropd  20576  islss  20920  lsslss  20947  lsspropd  21004  lsmelpr  21078  lbspropd  21086  lsslinds  21821  ltbval  22031  opsrval  22034  mhpval  22115  isbasisg  22922  tgval  22930  tgss3  22961  restbas  23133  tgrest  23134  restcld  23147  restopn2  23152  restntr  23157  cnpnei  23239  cncls2  23248  perfcls  23340  cmpsublem  23374  cmpsub  23375  cmpcld  23377  uncmp  23378  hauscmplem  23381  cmpfi  23383  nconnsubb  23398  clsconn  23405  hausllycmp  23469  1stckgenlem  23528  txbas  23542  ptbasfi  23556  txcnpi  23583  ptcnp  23597  txcmplem1  23616  txcmplem2  23617  xkococnlem  23634  qtopcld  23688  fbasssin  23811  fbssint  23813  fbun  23815  fbasrn  23859  filufint  23895  ufinffr  23904  ufildr  23906  ustval  24178  trust  24204  elmopn  24417  neibl  24476  cfilucfil  24534  icccmplem1  24798  icccmplem2  24799  bndth  24935  isphtpc  24971  metcld  25283  bcthlem1  25301  bcth  25306  ovolfioo  25444  ovolficc  25445  elovolmr  25453  ovoliunlem3  25481  ovolicc2  25499  volsuplem  25532  dyadmax  25575  dyadmbllem  25576  dyadmbl  25577  precsexlem6  28218  precsexlem7  28219  bdayfinbndlem1  28473  bdayfinbndlem2  28474  incistruhgr  29162  edgssv2  29281  wksfval  29693  2wlkdlem9  30017  3wlkdlem9  30253  sspval  30809  ubth  30959  orthin  31532  chssoc  31582  chsscon3  31586  chsscon1  31587  h1datom  31668  pjoml6i  31675  osum  31731  spansncv  31739  pjcjt2  31778  pjopyth  31806  hstel2  32305  hstle  32316  stj  32321  dmdbr5  32394  mdslmd1lem1  32411  atord  32474  chirredlem4  32479  atcvat4i  32483  mdsymlem2  32490  mdsymlem3  32491  mdsymlem8  32496  padct  32806  ssnnssfz  32875  pwrssmgc  33075  lindspropd  33458  idlsrgval  33578  constr01  33902  constrmon  33904  constrextdg2lem  33908  constrextdg2  33909  constrfiss  33911  tpr2rico  34072  ordtrestNEW  34081  sigaval  34271  issiga  34272  issgon  34283  oms0  34457  omssubadd  34460  subgrwlk  35330  umgr2cycllem  35338  kur14  35414  cvmliftlem15  35496  satfsschain  35562  mclsrcl  35759  mclsval  35761  ivthALT  36533  isfne  36537  topfne  36552  neibastop3  36560  tailfb  36575  filnetlem1  36576  filnetlem4  36579  relowlssretop  37693  rdgssun  37708  poimirlem24  37979  mblfinlem2  37993  sstotbnd2  38109  sstotbnd  38110  sstotbnd3  38111  ssbnd  38123  cntotbnd  38131  cnpwstotbnd  38132  ismtyres  38143  heibor1lem  38144  heiborlem1  38146  heiborlem6  38151  heiborlem8  38153  exidreslem  38212  scottexf  38503  scott0f  38504  cnvref4  38685  dfrefrels2  38928  dfrefrel2  38930  lshpcmp  39448  lsmsat  39468  lsmsatcv  39470  lfl1dim  39581  lfl1dim2N  39582  lkrss2N  39629  psubspset  40204  paddss  40305  psubclsetN  40396  dilfsetN  40612  dilsetN  40613  diaglbN  41515  dibglbN  41626  dihlspsnat  41793  dihglb2  41802  dochffval  41809  dochfval  41810  dochvalr  41817  dochord2N  41831  dochsncom  41842  dihjat1lem  41888  dvh4dimat  41898  dvh3dimatN  41899  dvh2dimatN  41900  dochexmidlem1  41920  lpolsetN  41942  lpolconN  41947  hdmaplkr  42373  hdmapoc  42391  hlhillcs  42418  ismrc  43147  incssnn0  43157  nacsfix  43158  hbt  43576  oacl2g  43776  omcl2  43779  ofoaf  43801  naddwordnexlem4  43847  ss2iundf  44104  clsk1indlem1  44490  clsk1independent  44491  isotone1  44493  isotone2  44494  ntrclsiso  44512  ntrclsk2  44513  scottelrankd  44692  ssinc  45535  uzfissfz  45774  stoweidlem50  46496  stoweidlem57  46503  fourierdlem20  46573  fourierdlem50  46602  fourierdlem64  46616  fourierdlem86  46638  fourierdlem103  46655  fourierdlem104  46656  ovnval  46987  hoicvrrex  47002  ovnlecvr  47004  ovncvrrp  47010  ovnsubaddlem1  47016  hoidmvlelem3  47043  hoidmvle  47046  ovnhoilem1  47047  ovnhoi  47049  ovnlecvr2  47056  ovncvr2  47057  hspmbl  47075  ovolval4lem2  47096  ovolval5lem2  47099  ovolval5lem3  47100  ovolval5  47101  ovnovollem1  47102  ovnovollem2  47103  sprsymrelfvlem  47962  grlimedgclnbgr  48483  grlimgrtri  48491  grilcbri2  48499  uspgrsprf  48634  uspgrsprfo  48636  ssnn0ssfz  48837  lincfsuppcl  48901  iunlub  49308  lubeldm2d  49445  glbeldm2d  49446