Theorem sseq2d 3962

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseq12d  3963  sseqtrd  3966  sbcrel  5725  funimass2  6570  fnssresb  6609  fnimaeq0  6620  foimacnv  6786  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  9084  fissuni  9247  dffi3  9321  cantnfle  9567  cantnflem1  9585  trcl  9624  r1sdom  9673  iscard2  9875  alephordi  9971  alephgeom  9979  cardaleph  9986  cardalephex  9987  ackbij2lem4  10138  cflm  10147  cfslbn  10164  cofsmo  10166  cfsmolem  10167  cfcoflem  10169  coftr  10170  alephsing  10173  fin23lem28  10237  fin23lem30  10239  fin23lem33  10242  fin1a2lem9  10305  axdc3lem2  10348  ttukeylem5  10410  pwfseqlem4a  10558  pwfseqlem4  10559  wunex2  10635  inar1  10672  sstskm  10739  fsuppmapnn0fiubex  13905  swrdnd  14568  swrd0  14572  repswswrd  14697  rtrclreclem1  14970  rtrclreclem2  14972  summolem2  15629  summo  15630  zsum  15631  sumz  15635  sumss  15637  fsumcvg3  15642  prodmolem2  15848  prodmo  15849  zprod  15850  prod1  15857  vdwlem1  16899  vdwlem12  16910  vdwlem13  16911  ramub2  16932  rami  16933  ramz2  16942  setsstruct2  17091  prdsval  17365  pwsle  17402  mrcuni  17533  gsumpropd  18592  gsumpropd2lem  18593  gsumress  18596  eqgfval  19094  sscntz  19244  resscntz  19251  lsmlub  19582  efgrelexlemb  19668  efgcpbllemb  19673  gsumval3a  19821  gsumzaddlem  19839  gsumzoppg  19862  dmdprd  19918  dprdcntz  19928  subgdmdprd  19954  subrngpropd  20489  subrgpropd  20529  islss  20873  lsslss  20900  lsspropd  20957  lsmelpr  21031  lbspropd  21039  lsslinds  21774  ltbval  21984  opsrval  21987  mhpval  22060  isbasisg  22868  tgval  22876  tgss3  22907  restbas  23079  tgrest  23080  restcld  23093  restopn2  23098  restntr  23103  cnpnei  23185  cncls2  23194  perfcls  23286  cmpsublem  23320  cmpsub  23321  cmpcld  23323  uncmp  23324  hauscmplem  23327  cmpfi  23329  nconnsubb  23344  clsconn  23351  hausllycmp  23415  1stckgenlem  23474  txbas  23488  ptbasfi  23502  txcnpi  23529  ptcnp  23543  txcmplem1  23562  txcmplem2  23563  xkococnlem  23580  qtopcld  23634  fbasssin  23757  fbssint  23759  fbun  23761  fbasrn  23805  filufint  23841  ufinffr  23850  ufildr  23852  ustval  24124  trust  24150  elmopn  24363  neibl  24422  cfilucfil  24480  icccmplem1  24744  icccmplem2  24745  bndth  24890  isphtpc  24926  metcld  25239  bcthlem1  25257  bcth  25262  ovolfioo  25401  ovolficc  25402  elovolmr  25410  ovoliunlem3  25438  ovolicc2  25456  volsuplem  25489  dyadmax  25532  dyadmbllem  25533  dyadmbl  25534  precsexlem6  28156  precsexlem7  28157  incistruhgr  29064  edgssv2  29183  wksfval  29595  2wlkdlem9  29919  3wlkdlem9  30155  sspval  30710  ubth  30860  orthin  31433  chssoc  31483  chsscon3  31487  chsscon1  31488  h1datom  31569  pjoml6i  31576  osum  31632  spansncv  31640  pjcjt2  31679  pjopyth  31707  hstel2  32206  hstle  32217  stj  32222  dmdbr5  32295  mdslmd1lem1  32312  atord  32375  chirredlem4  32380  atcvat4i  32384  mdsymlem2  32391  mdsymlem3  32392  mdsymlem8  32397  padct  32708  ssnnssfz  32777  pwrssmgc  32988  lindspropd  33355  idlsrgval  33475  constr01  33762  constrmon  33764  constrextdg2lem  33768  constrextdg2  33769  constrfiss  33771  tpr2rico  33932  ordtrestNEW  33941  sigaval  34131  issiga  34132  issgon  34143  oms0  34317  omssubadd  34320  subgrwlk  35183  umgr2cycllem  35191  kur14  35267  cvmliftlem15  35349  satfsschain  35415  mclsrcl  35612  mclsval  35614  ivthALT  36386  isfne  36390  topfne  36405  neibastop3  36413  tailfb  36428  filnetlem1  36429  filnetlem4  36432  relowlssretop  37414  rdgssun  37429  poimirlem24  37690  mblfinlem2  37704  sstotbnd2  37820  sstotbnd  37821  sstotbnd3  37822  ssbnd  37834  cntotbnd  37842  cnpwstotbnd  37843  ismtyres  37854  heibor1lem  37855  heiborlem1  37857  heiborlem6  37862  heiborlem8  37864  exidreslem  37923  scottexf  38214  scott0f  38215  cnvref4  38388  dfrefrels2  38611  dfrefrel2  38613  lshpcmp  39093  lsmsat  39113  lsmsatcv  39115  lfl1dim  39226  lfl1dim2N  39227  lkrss2N  39274  psubspset  39849  paddss  39950  psubclsetN  40041  dilfsetN  40257  dilsetN  40258  diaglbN  41160  dibglbN  41271  dihlspsnat  41438  dihglb2  41447  dochffval  41454  dochfval  41455  dochvalr  41462  dochord2N  41476  dochsncom  41487  dihjat1lem  41533  dvh4dimat  41543  dvh3dimatN  41544  dvh2dimatN  41545  dochexmidlem1  41565  lpolsetN  41587  lpolconN  41592  hdmaplkr  42018  hdmapoc  42036  hlhillcs  42063  ismrc  42799  incssnn0  42809  nacsfix  42810  hbt  43228  oacl2g  43428  omcl2  43431  ofoaf  43453  naddwordnexlem4  43499  ss2iundf  43757  clsk1indlem1  44143  clsk1independent  44144  isotone1  44146  isotone2  44147  ntrclsiso  44165  ntrclsk2  44166  scottelrankd  44345  ssinc  45189  uzfissfz  45430  stoweidlem50  46153  stoweidlem57  46160  fourierdlem20  46230  fourierdlem50  46259  fourierdlem64  46273  fourierdlem86  46295  fourierdlem103  46312  fourierdlem104  46313  ovnval  46644  hoicvrrex  46659  ovnlecvr  46661  ovncvrrp  46667  ovnsubaddlem1  46673  hoidmvlelem3  46700  hoidmvle  46703  ovnhoilem1  46704  ovnhoi  46706  ovnlecvr2  46713  ovncvr2  46714  hspmbl  46732  ovolval4lem2  46753  ovolval5lem2  46756  ovolval5lem3  46757  ovolval5  46758  ovnovollem1  46759  ovnovollem2  46760  sprsymrelfvlem  47595  grlimedgclnbgr  48100  grlimgrtri  48108  grilcbri2  48116  uspgrsprf  48251  uspgrsprfo  48253  ssnn0ssfz  48454  lincfsuppcl  48519  iunlub  48926  lubeldm2d  49063  glbeldm2d  49064