Theorem sseq2d 3963

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseq12d  3964  sseqtrd  3967  sbcrel  5725  funimass2  6569  fnssresb  6608  fnimaeq0  6619  foimacnv  6785  fvelimab  6900  ssimaexg  6914  ralima  7177  knatar  7297  frecseq123  8218  frrlem4  8225  onfununi  8267  oaordi  8467  oawordeulem  8475  oaass  8482  odi  8500  omass  8501  oen0  8507  oelim2  8516  nnaordi  8539  nnawordex  8558  naddunif  8614  pssnn  9085  fissuni  9248  dffi3  9322  cantnfle  9568  cantnflem1  9586  trcl  9625  r1sdom  9674  iscard2  9876  alephordi  9972  alephgeom  9980  cardaleph  9987  cardalephex  9988  ackbij2lem4  10139  cflm  10148  cfslbn  10165  cofsmo  10167  cfsmolem  10168  cfcoflem  10170  coftr  10171  alephsing  10174  fin23lem28  10238  fin23lem30  10240  fin23lem33  10243  fin1a2lem9  10306  axdc3lem2  10349  ttukeylem5  10411  pwfseqlem4a  10559  pwfseqlem4  10560  wunex2  10636  inar1  10673  sstskm  10740  fsuppmapnn0fiubex  13901  swrdnd  14564  swrd0  14568  repswswrd  14693  rtrclreclem1  14966  rtrclreclem2  14968  summolem2  15625  summo  15626  zsum  15627  sumz  15631  sumss  15633  fsumcvg3  15638  prodmolem2  15844  prodmo  15845  zprod  15846  prod1  15853  vdwlem1  16895  vdwlem12  16906  vdwlem13  16907  ramub2  16928  rami  16929  ramz2  16938  setsstruct2  17087  prdsval  17361  pwsle  17398  mrcuni  17529  gsumpropd  18588  gsumpropd2lem  18589  gsumress  18592  eqgfval  19090  sscntz  19240  resscntz  19247  lsmlub  19578  efgrelexlemb  19664  efgcpbllemb  19669  gsumval3a  19817  gsumzaddlem  19835  gsumzoppg  19858  dmdprd  19914  dprdcntz  19924  subgdmdprd  19950  subrngpropd  20485  subrgpropd  20525  islss  20869  lsslss  20896  lsspropd  20953  lsmelpr  21027  lbspropd  21035  lsslinds  21770  ltbval  21979  opsrval  21982  mhpval  22055  isbasisg  22863  tgval  22871  tgss3  22902  restbas  23074  tgrest  23075  restcld  23088  restopn2  23093  restntr  23098  cnpnei  23180  cncls2  23189  perfcls  23281  cmpsublem  23315  cmpsub  23316  cmpcld  23318  uncmp  23319  hauscmplem  23322  cmpfi  23324  nconnsubb  23339  clsconn  23346  hausllycmp  23410  1stckgenlem  23469  txbas  23483  ptbasfi  23497  txcnpi  23524  ptcnp  23538  txcmplem1  23557  txcmplem2  23558  xkococnlem  23575  qtopcld  23629  fbasssin  23752  fbssint  23754  fbun  23756  fbasrn  23800  filufint  23836  ufinffr  23845  ufildr  23847  ustval  24119  trust  24145  elmopn  24358  neibl  24417  cfilucfil  24475  icccmplem1  24739  icccmplem2  24740  bndth  24885  isphtpc  24921  metcld  25234  bcthlem1  25252  bcth  25257  ovolfioo  25396  ovolficc  25397  elovolmr  25405  ovoliunlem3  25433  ovolicc2  25451  volsuplem  25484  dyadmax  25527  dyadmbllem  25528  dyadmbl  25529  precsexlem6  28151  precsexlem7  28152  incistruhgr  29059  edgssv2  29178  wksfval  29590  2wlkdlem9  29914  3wlkdlem9  30150  sspval  30705  ubth  30855  orthin  31428  chssoc  31478  chsscon3  31482  chsscon1  31483  h1datom  31564  pjoml6i  31571  osum  31627  spansncv  31635  pjcjt2  31674  pjopyth  31702  hstel2  32201  hstle  32212  stj  32217  dmdbr5  32290  mdslmd1lem1  32307  atord  32370  chirredlem4  32375  atcvat4i  32379  mdsymlem2  32386  mdsymlem3  32387  mdsymlem8  32392  padct  32705  ssnnssfz  32774  pwrssmgc  32988  lindspropd  33355  idlsrgval  33475  constr01  33776  constrmon  33778  constrextdg2lem  33782  constrextdg2  33783  constrfiss  33785  tpr2rico  33946  ordtrestNEW  33955  sigaval  34145  issiga  34146  issgon  34157  oms0  34331  omssubadd  34334  subgrwlk  35197  umgr2cycllem  35205  kur14  35281  cvmliftlem15  35363  satfsschain  35429  mclsrcl  35626  mclsval  35628  ivthALT  36400  isfne  36404  topfne  36419  neibastop3  36427  tailfb  36442  filnetlem1  36443  filnetlem4  36446  relowlssretop  37428  rdgssun  37443  poimirlem24  37704  mblfinlem2  37718  sstotbnd2  37834  sstotbnd  37835  sstotbnd3  37836  ssbnd  37848  cntotbnd  37856  cnpwstotbnd  37857  ismtyres  37868  heibor1lem  37869  heiborlem1  37871  heiborlem6  37876  heiborlem8  37878  exidreslem  37937  scottexf  38228  scott0f  38229  cnvref4  38402  dfrefrels2  38625  dfrefrel2  38627  lshpcmp  39107  lsmsat  39127  lsmsatcv  39129  lfl1dim  39240  lfl1dim2N  39241  lkrss2N  39288  psubspset  39863  paddss  39964  psubclsetN  40055  dilfsetN  40271  dilsetN  40272  diaglbN  41174  dibglbN  41285  dihlspsnat  41452  dihglb2  41461  dochffval  41468  dochfval  41469  dochvalr  41476  dochord2N  41490  dochsncom  41501  dihjat1lem  41547  dvh4dimat  41557  dvh3dimatN  41558  dvh2dimatN  41559  dochexmidlem1  41579  lpolsetN  41601  lpolconN  41606  hdmaplkr  42032  hdmapoc  42050  hlhillcs  42077  ismrc  42818  incssnn0  42828  nacsfix  42829  hbt  43247  oacl2g  43447  omcl2  43450  ofoaf  43472  naddwordnexlem4  43518  ss2iundf  43776  clsk1indlem1  44162  clsk1independent  44163  isotone1  44165  isotone2  44166  ntrclsiso  44184  ntrclsk2  44185  scottelrankd  44364  ssinc  45208  uzfissfz  45449  stoweidlem50  46172  stoweidlem57  46179  fourierdlem20  46249  fourierdlem50  46278  fourierdlem64  46292  fourierdlem86  46314  fourierdlem103  46331  fourierdlem104  46332  ovnval  46663  hoicvrrex  46678  ovnlecvr  46680  ovncvrrp  46686  ovnsubaddlem1  46692  hoidmvlelem3  46719  hoidmvle  46722  ovnhoilem1  46723  ovnhoi  46725  ovnlecvr2  46732  ovncvr2  46733  hspmbl  46751  ovolval4lem2  46772  ovolval5lem2  46775  ovolval5lem3  46776  ovolval5  46777  ovnovollem1  46778  ovnovollem2  46779  sprsymrelfvlem  47614  grlimedgclnbgr  48119  grlimgrtri  48127  grilcbri2  48135  uspgrsprf  48270  uspgrsprfo  48272  ssnn0ssfz  48473  lincfsuppcl  48538  iunlub  48945  lubeldm2d  49082  glbeldm2d  49083