Theorem sseq2d 3991

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sseq12d  3992  sseqtrd  3995  sbcrel  5759  funimass2  6618  fnssresb  6659  fnimaeq0  6670  foimacnv  6834  fvelimab  6950  ssimaexg  6964  ralima  7228  knatar  7349  frecseq123  8279  frrlem4  8286  wfrdmclOLD  8329  wfrlem12OLD  8332  onfununi  8353  oaordi  8556  oawordeulem  8564  oaass  8571  odi  8589  omass  8590  oen0  8596  oelim2  8605  nnaordi  8628  nnawordex  8647  naddunif  8703  pssnn  9180  fissuni  9367  dffi3  9441  cantnfle  9683  cantnflem1  9701  trcl  9740  r1sdom  9786  iscard2  9988  alephordi  10086  alephgeom  10094  cardaleph  10101  cardalephex  10102  ackbij2lem4  10253  cflm  10262  cfslbn  10279  cofsmo  10281  cfsmolem  10282  cfcoflem  10284  coftr  10285  alephsing  10288  fin23lem28  10352  fin23lem30  10354  fin23lem33  10357  fin1a2lem9  10420  axdc3lem2  10463  ttukeylem5  10525  pwfseqlem4a  10673  pwfseqlem4  10674  wunex2  10750  inar1  10787  sstskm  10854  fsuppmapnn0fiubex  14008  swrdnd  14670  swrd0  14674  repswswrd  14800  rtrclreclem1  15074  rtrclreclem2  15076  summolem2  15730  summo  15731  zsum  15732  sumz  15736  sumss  15738  fsumcvg3  15743  prodmolem2  15949  prodmo  15950  zprod  15951  prod1  15958  vdwlem1  16999  vdwlem12  17010  vdwlem13  17011  ramub2  17032  rami  17033  ramz2  17042  setsstruct2  17191  prdsval  17467  pwsle  17504  mrcuni  17631  gsumpropd  18654  gsumpropd2lem  18655  gsumress  18658  eqgfval  19157  sscntz  19307  resscntz  19314  lsmlub  19643  efgrelexlemb  19729  efgcpbllemb  19734  gsumval3a  19882  gsumzaddlem  19900  gsumzoppg  19923  dmdprd  19979  dprdcntz  19989  subgdmdprd  20015  subrngpropd  20526  subrgpropd  20566  islss  20889  lsslss  20916  lsspropd  20973  lsmelpr  21047  lbspropd  21055  lsslinds  21789  ltbval  21999  opsrval  22002  mhpval  22075  isbasisg  22883  tgval  22891  tgss3  22922  restbas  23094  tgrest  23095  restcld  23108  restopn2  23113  restntr  23118  cnpnei  23200  cncls2  23209  perfcls  23301  cmpsublem  23335  cmpsub  23336  cmpcld  23338  uncmp  23339  hauscmplem  23342  cmpfi  23344  nconnsubb  23359  clsconn  23366  hausllycmp  23430  1stckgenlem  23489  txbas  23503  ptbasfi  23517  txcnpi  23544  ptcnp  23558  txcmplem1  23577  txcmplem2  23578  xkococnlem  23595  qtopcld  23649  fbasssin  23772  fbssint  23774  fbun  23776  fbasrn  23820  filufint  23856  ufinffr  23865  ufildr  23867  ustval  24139  trust  24166  elmopn  24379  neibl  24438  cfilucfil  24496  icccmplem1  24760  icccmplem2  24761  bndth  24906  isphtpc  24942  metcld  25256  bcthlem1  25274  bcth  25279  ovolfioo  25418  ovolficc  25419  elovolmr  25427  ovoliunlem3  25455  ovolicc2  25473  volsuplem  25506  dyadmax  25549  dyadmbllem  25550  dyadmbl  25551  precsexlem6  28153  precsexlem7  28154  incistruhgr  29004  edgssv2  29123  wksfval  29535  2wlkdlem9  29862  3wlkdlem9  30095  sspval  30650  ubth  30800  orthin  31373  chssoc  31423  chsscon3  31427  chsscon1  31428  h1datom  31509  pjoml6i  31516  osum  31572  spansncv  31580  pjcjt2  31619  pjopyth  31647  hstel2  32146  hstle  32157  stj  32162  dmdbr5  32235  mdslmd1lem1  32252  atord  32315  chirredlem4  32320  atcvat4i  32324  mdsymlem2  32331  mdsymlem3  32332  mdsymlem8  32337  padct  32643  ssnnssfz  32710  pwrssmgc  32926  lindspropd  33344  idlsrgval  33464  constr01  33722  constrmon  33724  constrextdg2lem  33728  constrextdg2  33729  constrfiss  33731  tpr2rico  33889  ordtrestNEW  33898  sigaval  34088  issiga  34089  issgon  34100  oms0  34275  omssubadd  34278  subgrwlk  35100  umgr2cycllem  35108  kur14  35184  cvmliftlem15  35266  satfsschain  35332  mclsrcl  35529  mclsval  35531  ivthALT  36299  isfne  36303  topfne  36318  neibastop3  36326  tailfb  36341  filnetlem1  36342  filnetlem4  36345  relowlssretop  37327  rdgssun  37342  poimirlem24  37614  mblfinlem2  37628  sstotbnd2  37744  sstotbnd  37745  sstotbnd3  37746  ssbnd  37758  cntotbnd  37766  cnpwstotbnd  37767  ismtyres  37778  heibor1lem  37779  heiborlem1  37781  heiborlem6  37786  heiborlem8  37788  exidreslem  37847  scottexf  38138  scott0f  38139  cnvref4  38314  dfrefrels2  38477  dfrefrel2  38479  lshpcmp  38952  lsmsat  38972  lsmsatcv  38974  lfl1dim  39085  lfl1dim2N  39086  lkrss2N  39133  psubspset  39709  paddss  39810  psubclsetN  39901  dilfsetN  40117  dilsetN  40118  diaglbN  41020  dibglbN  41131  dihlspsnat  41298  dihglb2  41307  dochffval  41314  dochfval  41315  dochvalr  41322  dochord2N  41336  dochsncom  41347  dihjat1lem  41393  dvh4dimat  41403  dvh3dimatN  41404  dvh2dimatN  41405  dochexmidlem1  41425  lpolsetN  41447  lpolconN  41452  hdmaplkr  41878  hdmapoc  41896  hlhillcs  41923  ismrc  42671  incssnn0  42681  nacsfix  42682  hbt  43101  oacl2g  43301  omcl2  43304  ofoaf  43326  naddwordnexlem4  43372  ss2iundf  43630  clsk1indlem1  44016  clsk1independent  44017  isotone1  44019  isotone2  44020  ntrclsiso  44038  ntrclsk2  44039  scottelrankd  44219  ssinc  45059  uzfissfz  45301  stoweidlem50  46027  stoweidlem57  46034  fourierdlem20  46104  fourierdlem50  46133  fourierdlem64  46147  fourierdlem86  46169  fourierdlem103  46186  fourierdlem104  46187  ovnval  46518  hoicvrrex  46533  ovnlecvr  46535  ovncvrrp  46541  ovnsubaddlem1  46547  hoidmvlelem3  46574  hoidmvle  46577  ovnhoilem1  46578  ovnhoi  46580  ovnlecvr2  46587  ovncvr2  46588  hspmbl  46606  ovolval4lem2  46627  ovolval5lem2  46630  ovolval5lem3  46631  ovolval5  46632  ovnovollem1  46633  ovnovollem2  46634  sprsymrelfvlem  47452  grlimgrtri  47956  grilcbri2  47964  uspgrsprf  48069  uspgrsprfo  48071  ssnn0ssfz  48272  lincfsuppcl  48337  iunlub  48747  lubeldm2d  48880  glbeldm2d  48881