Theorem sseq2d 4009

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  sseq12d  4010  sseqtrd  4017  sbcrel  5782  funimass2  6637  fncoOLD  6674  fnssresb  6678  fnimaeq0  6689  foimacnv  6855  fvelimab  6970  ssimaexg  6983  knatar  7364  frecseq123  8288  frrlem4  8295  wfrdmclOLD  8338  wfrlem12OLD  8341  onfununi  8362  oaordi  8567  oawordeulem  8575  oaass  8582  odi  8600  omass  8601  oen0  8607  oelim2  8616  nnaordi  8639  nnawordex  8658  naddunif  8714  pssnn  9193  pssnnOLD  9290  fissuni  9383  dffi3  9456  cantnfle  9696  cantnflem1  9714  trcl  9753  r1sdom  9799  iscard2  10001  alephordi  10099  alephgeom  10107  cardaleph  10114  cardalephex  10115  ackbij2lem4  10267  cflm  10275  cfslbn  10292  cofsmo  10294  cfsmolem  10295  cfcoflem  10297  coftr  10298  alephsing  10301  fin23lem28  10365  fin23lem30  10367  fin23lem33  10370  fin1a2lem9  10433  axdc3lem2  10476  ttukeylem5  10538  fpwwe2lem4  10659  pwfseqlem4a  10686  pwfseqlem4  10687  wunex2  10763  inar1  10800  sstskm  10867  fsuppmapnn0fiubex  13993  swrdnd  14640  swrd0  14644  repswswrd  14770  rtrclreclem1  15040  rtrclreclem2  15042  summolem2  15698  summo  15699  zsum  15700  sumz  15704  sumss  15706  fsumcvg3  15711  prodmolem2  15915  prodmo  15916  zprod  15917  prod1  15924  vdwlem1  16953  vdwlem12  16964  vdwlem13  16965  ramub2  16986  rami  16987  ramz2  16996  setsstruct2  17146  prdsval  17440  pwsle  17477  mrcuni  17604  gsumpropd  18641  gsumpropd2lem  18642  gsumress  18645  eqgfval  19139  sscntz  19289  resscntz  19296  lsmlub  19631  efgrelexlemb  19717  efgcpbllemb  19722  gsumval3a  19870  gsumzaddlem  19888  gsumzoppg  19911  dmdprd  19967  dprdcntz  19977  subgdmdprd  20003  subrngpropd  20517  subrgpropd  20559  islss  20830  lsslss  20857  lsspropd  20914  lsmelpr  20988  lbspropd  20996  lsslinds  21782  ltbval  22003  opsrval  22006  mhpval  22087  isbasisg  22894  tgval  22902  tgss3  22933  restbas  23106  tgrest  23107  restcld  23120  restopn2  23125  restntr  23130  cnpnei  23212  cncls2  23221  perfcls  23313  cmpsublem  23347  cmpsub  23348  cmpcld  23350  uncmp  23351  hauscmplem  23354  cmpfi  23356  nconnsubb  23371  clsconn  23378  hausllycmp  23442  1stckgenlem  23501  txbas  23515  ptbasfi  23529  txcnpi  23556  ptcnp  23570  txcmplem1  23589  txcmplem2  23590  xkococnlem  23607  qtopcld  23661  fbasssin  23784  fbssint  23786  fbun  23788  fbasrn  23832  filufint  23868  ufinffr  23877  ufildr  23879  ustval  24151  trust  24178  elmopn  24392  neibl  24454  cfilucfil  24512  icccmplem1  24782  icccmplem2  24783  bndth  24928  isphtpc  24964  metcld  25278  bcthlem1  25296  bcth  25301  ovolfioo  25440  ovolficc  25441  elovolmr  25449  ovoliunlem3  25477  ovolicc2  25495  volsuplem  25528  dyadmax  25571  dyadmbllem  25572  dyadmbl  25573  precsexlem6  28160  precsexlem7  28161  incistruhgr  28964  edgssv2  29083  wksfval  29495  2wlkdlem9  29817  3wlkdlem9  30050  sspval  30605  ubth  30755  orthin  31328  chssoc  31378  chsscon3  31382  chsscon1  31383  h1datom  31464  pjoml6i  31471  osum  31527  spansncv  31535  pjcjt2  31574  pjopyth  31602  hstel2  32101  hstle  32112  stj  32117  dmdbr5  32190  mdslmd1lem1  32207  atord  32270  chirredlem4  32275  atcvat4i  32279  mdsymlem2  32286  mdsymlem3  32287  mdsymlem8  32292  padct  32583  ssnnssfz  32637  pwrssmgc  32816  lindspropd  33195  idlsrgval  33315  tpr2rico  33644  ordtrestNEW  33653  sigaval  33861  issiga  33862  issgon  33873  oms0  34048  omssubadd  34051  subgrwlk  34873  umgr2cycllem  34881  kur14  34957  cvmliftlem15  35039  satfsschain  35105  mclsrcl  35302  mclsval  35304  ivthALT  35950  isfne  35954  topfne  35969  neibastop3  35977  tailfb  35992  filnetlem1  35993  filnetlem4  35996  relowlssretop  36973  rdgssun  36988  poimirlem24  37248  mblfinlem2  37262  sstotbnd2  37378  sstotbnd  37379  sstotbnd3  37380  ssbnd  37392  cntotbnd  37400  cnpwstotbnd  37401  ismtyres  37412  heibor1lem  37413  heiborlem1  37415  heiborlem6  37420  heiborlem8  37422  exidreslem  37481  scottexf  37772  scott0f  37773  cnvref4  37952  dfrefrels2  38115  dfrefrel2  38117  lshpcmp  38590  lsmsat  38610  lsmsatcv  38612  lfl1dim  38723  lfl1dim2N  38724  lkrss2N  38771  psubspset  39347  paddss  39448  psubclsetN  39539  dilfsetN  39755  dilsetN  39756  diaglbN  40658  dibglbN  40769  dihlspsnat  40936  dihglb2  40945  dochffval  40952  dochfval  40953  dochvalr  40960  dochord2N  40974  dochsncom  40985  dihjat1lem  41031  dvh4dimat  41041  dvh3dimatN  41042  dvh2dimatN  41043  dochexmidlem1  41063  lpolsetN  41085  lpolconN  41090  hdmaplkr  41516  hdmapoc  41534  hlhillcs  41565  ismrc  42263  incssnn0  42273  nacsfix  42274  hbt  42696  oacl2g  42901  omcl2  42904  ofoaf  42926  naddwordnexlem4  42973  ss2iundf  43231  clsk1indlem1  43617  clsk1independent  43618  isotone1  43620  isotone2  43621  ntrclsiso  43639  ntrclsk2  43640  scottelrankd  43826  ssinc  44593  uzfissfz  44846  stoweidlem50  45576  stoweidlem57  45583  fourierdlem20  45653  fourierdlem50  45682  fourierdlem64  45696  fourierdlem86  45718  fourierdlem103  45735  fourierdlem104  45736  ovnval  46067  hoicvrrex  46082  ovnlecvr  46084  ovncvrrp  46090  ovnsubaddlem1  46096  hoidmvlelem3  46123  hoidmvle  46126  ovnhoilem1  46127  ovnhoi  46129  ovnlecvr2  46136  ovncvr2  46137  hspmbl  46155  ovolval4lem2  46176  ovolval5lem2  46179  ovolval5lem3  46180  ovolval5  46181  ovnovollem1  46182  ovnovollem2  46183  sprsymrelfvlem  46967  uspgrsprf  47394  uspgrsprfo  47396  ssnn0ssfz  47599  lincfsuppcl  47667  lubeldm2d  48163  glbeldm2d  48164