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 17	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseq12d  3971  sseqtrd  3974  sbcrel  5728  funimass2  6569  fnssresb  6608  fnimaeq0  6619  foimacnv  6785  fvelimab  6899  ssimaexg  6913  ralima  7177  knatar  7298  frecseq123  8222  frrlem4  8229  onfununi  8271  oaordi  8471  oawordeulem  8479  oaass  8486  odi  8504  omass  8505  oen0  8511  oelim2  8520  nnaordi  8543  nnawordex  8562  naddunif  8618  pssnn  9092  fissuni  9266  dffi3  9340  cantnfle  9586  cantnflem1  9604  trcl  9643  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  10574  pwfseqlem4  10575  wunex2  10651  inar1  10688  sstskm  10755  fsuppmapnn0fiubex  13917  swrdnd  14579  swrd0  14583  repswswrd  14708  rtrclreclem1  14982  rtrclreclem2  14984  summolem2  15641  summo  15642  zsum  15643  sumz  15647  sumss  15649  fsumcvg3  15654  prodmolem2  15860  prodmo  15861  zprod  15862  prod1  15869  vdwlem1  16911  vdwlem12  16922  vdwlem13  16923  ramub2  16944  rami  16945  ramz2  16954  setsstruct2  17103  prdsval  17377  pwsle  17414  mrcuni  17545  gsumpropd  18570  gsumpropd2lem  18571  gsumress  18574  eqgfval  19073  sscntz  19223  resscntz  19230  lsmlub  19561  efgrelexlemb  19647  efgcpbllemb  19652  gsumval3a  19800  gsumzaddlem  19818  gsumzoppg  19841  dmdprd  19897  dprdcntz  19907  subgdmdprd  19933  subrngpropd  20471  subrgpropd  20511  islss  20855  lsslss  20882  lsspropd  20939  lsmelpr  21013  lbspropd  21021  lsslinds  21756  ltbval  21966  opsrval  21969  mhpval  22042  isbasisg  22850  tgval  22858  tgss3  22889  restbas  23061  tgrest  23062  restcld  23075  restopn2  23080  restntr  23085  cnpnei  23167  cncls2  23176  perfcls  23268  cmpsublem  23302  cmpsub  23303  cmpcld  23305  uncmp  23306  hauscmplem  23309  cmpfi  23311  nconnsubb  23326  clsconn  23333  hausllycmp  23397  1stckgenlem  23456  txbas  23470  ptbasfi  23484  txcnpi  23511  ptcnp  23525  txcmplem1  23544  txcmplem2  23545  xkococnlem  23562  qtopcld  23616  fbasssin  23739  fbssint  23741  fbun  23743  fbasrn  23787  filufint  23823  ufinffr  23832  ufildr  23834  ustval  24106  trust  24133  elmopn  24346  neibl  24405  cfilucfil  24463  icccmplem1  24727  icccmplem2  24728  bndth  24873  isphtpc  24909  metcld  25222  bcthlem1  25240  bcth  25245  ovolfioo  25384  ovolficc  25385  elovolmr  25393  ovoliunlem3  25421  ovolicc2  25439  volsuplem  25472  dyadmax  25515  dyadmbllem  25516  dyadmbl  25517  precsexlem6  28137  precsexlem7  28138  incistruhgr  29042  edgssv2  29161  wksfval  29573  2wlkdlem9  29897  3wlkdlem9  30130  sspval  30685  ubth  30835  orthin  31408  chssoc  31458  chsscon3  31462  chsscon1  31463  h1datom  31544  pjoml6i  31551  osum  31607  spansncv  31615  pjcjt2  31654  pjopyth  31682  hstel2  32181  hstle  32192  stj  32197  dmdbr5  32270  mdslmd1lem1  32287  atord  32350  chirredlem4  32355  atcvat4i  32359  mdsymlem2  32366  mdsymlem3  32367  mdsymlem8  32372  padct  32676  ssnnssfz  32743  pwrssmgc  32955  lindspropd  33330  idlsrgval  33450  constr01  33708  constrmon  33710  constrextdg2lem  33714  constrextdg2  33715  constrfiss  33717  tpr2rico  33878  ordtrestNEW  33887  sigaval  34077  issiga  34078  issgon  34089  oms0  34264  omssubadd  34267  subgrwlk  35104  umgr2cycllem  35112  kur14  35188  cvmliftlem15  35270  satfsschain  35336  mclsrcl  35533  mclsval  35535  ivthALT  36308  isfne  36312  topfne  36327  neibastop3  36335  tailfb  36350  filnetlem1  36351  filnetlem4  36354  relowlssretop  37336  rdgssun  37351  poimirlem24  37623  mblfinlem2  37637  sstotbnd2  37753  sstotbnd  37754  sstotbnd3  37755  ssbnd  37767  cntotbnd  37775  cnpwstotbnd  37776  ismtyres  37787  heibor1lem  37788  heiborlem1  37790  heiborlem6  37795  heiborlem8  37797  exidreslem  37856  scottexf  38147  scott0f  38148  cnvref4  38317  dfrefrels2  38489  dfrefrel2  38491  lshpcmp  38966  lsmsat  38986  lsmsatcv  38988  lfl1dim  39099  lfl1dim2N  39100  lkrss2N  39147  psubspset  39723  paddss  39824  psubclsetN  39915  dilfsetN  40131  dilsetN  40132  diaglbN  41034  dibglbN  41145  dihlspsnat  41312  dihglb2  41321  dochffval  41328  dochfval  41329  dochvalr  41336  dochord2N  41350  dochsncom  41361  dihjat1lem  41407  dvh4dimat  41417  dvh3dimatN  41418  dvh2dimatN  41419  dochexmidlem1  41439  lpolsetN  41461  lpolconN  41466  hdmaplkr  41892  hdmapoc  41910  hlhillcs  41937  ismrc  42674  incssnn0  42684  nacsfix  42685  hbt  43103  oacl2g  43303  omcl2  43306  ofoaf  43328  naddwordnexlem4  43374  ss2iundf  43632  clsk1indlem1  44018  clsk1independent  44019  isotone1  44021  isotone2  44022  ntrclsiso  44040  ntrclsk2  44041  scottelrankd  44220  ssinc  45065  uzfissfz  45306  stoweidlem50  46032  stoweidlem57  46039  fourierdlem20  46109  fourierdlem50  46138  fourierdlem64  46152  fourierdlem86  46174  fourierdlem103  46191  fourierdlem104  46192  ovnval  46523  hoicvrrex  46538  ovnlecvr  46540  ovncvrrp  46546  ovnsubaddlem1  46552  hoidmvlelem3  46579  hoidmvle  46582  ovnhoilem1  46583  ovnhoi  46585  ovnlecvr2  46592  ovncvr2  46593  hspmbl  46611  ovolval4lem2  46632  ovolval5lem2  46635  ovolval5lem3  46636  ovolval5  46637  ovnovollem1  46638  ovnovollem2  46639  sprsymrelfvlem  47475  grlimedgclnbgr  47980  grlimgrtri  47988  grilcbri2  47996  uspgrsprf  48131  uspgrsprfo  48133  ssnn0ssfz  48334  lincfsuppcl  48399  iunlub  48806  lubeldm2d  48943  glbeldm2d  48944