Theorem sseq2d 3967

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

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

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 3919

This theorem is referenced by:  sseq12d  3968  sseqtrd  3971  sbcrel  5721  funimass2  6564  fnssresb  6603  fnimaeq0  6614  foimacnv  6780  fvelimab  6894  ssimaexg  6908  ralima  7171  knatar  7291  frecseq123  8212  frrlem4  8219  onfununi  8261  oaordi  8461  oawordeulem  8469  oaass  8476  odi  8494  omass  8495  oen0  8501  oelim2  8510  nnaordi  8533  nnawordex  8552  naddunif  8608  pssnn  9078  fissuni  9241  dffi3  9315  cantnfle  9561  cantnflem1  9579  trcl  9618  r1sdom  9664  iscard2  9866  alephordi  9962  alephgeom  9970  cardaleph  9977  cardalephex  9978  ackbij2lem4  10129  cflm  10138  cfslbn  10155  cofsmo  10157  cfsmolem  10158  cfcoflem  10160  coftr  10161  alephsing  10164  fin23lem28  10228  fin23lem30  10230  fin23lem33  10233  fin1a2lem9  10296  axdc3lem2  10339  ttukeylem5  10401  pwfseqlem4a  10549  pwfseqlem4  10550  wunex2  10626  inar1  10663  sstskm  10730  fsuppmapnn0fiubex  13896  swrdnd  14559  swrd0  14563  repswswrd  14688  rtrclreclem1  14961  rtrclreclem2  14963  summolem2  15620  summo  15621  zsum  15622  sumz  15626  sumss  15628  fsumcvg3  15633  prodmolem2  15839  prodmo  15840  zprod  15841  prod1  15848  vdwlem1  16890  vdwlem12  16901  vdwlem13  16902  ramub2  16923  rami  16924  ramz2  16933  setsstruct2  17082  prdsval  17356  pwsle  17393  mrcuni  17524  gsumpropd  18583  gsumpropd2lem  18584  gsumress  18587  eqgfval  19086  sscntz  19236  resscntz  19243  lsmlub  19574  efgrelexlemb  19660  efgcpbllemb  19665  gsumval3a  19813  gsumzaddlem  19831  gsumzoppg  19854  dmdprd  19910  dprdcntz  19920  subgdmdprd  19946  subrngpropd  20481  subrgpropd  20521  islss  20865  lsslss  20892  lsspropd  20949  lsmelpr  21023  lbspropd  21031  lsslinds  21766  ltbval  21976  opsrval  21979  mhpval  22052  isbasisg  22860  tgval  22868  tgss3  22899  restbas  23071  tgrest  23072  restcld  23085  restopn2  23090  restntr  23095  cnpnei  23177  cncls2  23186  perfcls  23278  cmpsublem  23312  cmpsub  23313  cmpcld  23315  uncmp  23316  hauscmplem  23319  cmpfi  23321  nconnsubb  23336  clsconn  23343  hausllycmp  23407  1stckgenlem  23466  txbas  23480  ptbasfi  23494  txcnpi  23521  ptcnp  23535  txcmplem1  23554  txcmplem2  23555  xkococnlem  23572  qtopcld  23626  fbasssin  23749  fbssint  23751  fbun  23753  fbasrn  23797  filufint  23833  ufinffr  23842  ufildr  23844  ustval  24116  trust  24142  elmopn  24355  neibl  24414  cfilucfil  24472  icccmplem1  24736  icccmplem2  24737  bndth  24882  isphtpc  24918  metcld  25231  bcthlem1  25249  bcth  25254  ovolfioo  25393  ovolficc  25394  elovolmr  25402  ovoliunlem3  25430  ovolicc2  25448  volsuplem  25481  dyadmax  25524  dyadmbllem  25525  dyadmbl  25526  precsexlem6  28148  precsexlem7  28149  incistruhgr  29055  edgssv2  29174  wksfval  29586  2wlkdlem9  29910  3wlkdlem9  30143  sspval  30698  ubth  30848  orthin  31421  chssoc  31471  chsscon3  31475  chsscon1  31476  h1datom  31557  pjoml6i  31564  osum  31620  spansncv  31628  pjcjt2  31667  pjopyth  31695  hstel2  32194  hstle  32205  stj  32210  dmdbr5  32283  mdslmd1lem1  32300  atord  32363  chirredlem4  32368  atcvat4i  32372  mdsymlem2  32379  mdsymlem3  32380  mdsymlem8  32385  padct  32696  ssnnssfz  32765  pwrssmgc  32976  lindspropd  33343  idlsrgval  33463  constr01  33750  constrmon  33752  constrextdg2lem  33756  constrextdg2  33757  constrfiss  33759  tpr2rico  33920  ordtrestNEW  33929  sigaval  34119  issiga  34120  issgon  34131  oms0  34305  omssubadd  34308  subgrwlk  35164  umgr2cycllem  35172  kur14  35248  cvmliftlem15  35330  satfsschain  35396  mclsrcl  35593  mclsval  35595  ivthALT  36368  isfne  36372  topfne  36387  neibastop3  36395  tailfb  36410  filnetlem1  36411  filnetlem4  36414  relowlssretop  37396  rdgssun  37411  poimirlem24  37683  mblfinlem2  37697  sstotbnd2  37813  sstotbnd  37814  sstotbnd3  37815  ssbnd  37827  cntotbnd  37835  cnpwstotbnd  37836  ismtyres  37847  heibor1lem  37848  heiborlem1  37850  heiborlem6  37855  heiborlem8  37857  exidreslem  37916  scottexf  38207  scott0f  38208  cnvref4  38377  dfrefrels2  38549  dfrefrel2  38551  lshpcmp  39026  lsmsat  39046  lsmsatcv  39048  lfl1dim  39159  lfl1dim2N  39160  lkrss2N  39207  psubspset  39782  paddss  39883  psubclsetN  39974  dilfsetN  40190  dilsetN  40191  diaglbN  41093  dibglbN  41204  dihlspsnat  41371  dihglb2  41380  dochffval  41387  dochfval  41388  dochvalr  41395  dochord2N  41409  dochsncom  41420  dihjat1lem  41466  dvh4dimat  41476  dvh3dimatN  41477  dvh2dimatN  41478  dochexmidlem1  41498  lpolsetN  41520  lpolconN  41525  hdmaplkr  41951  hdmapoc  41969  hlhillcs  41996  ismrc  42733  incssnn0  42743  nacsfix  42744  hbt  43162  oacl2g  43362  omcl2  43365  ofoaf  43387  naddwordnexlem4  43433  ss2iundf  43691  clsk1indlem1  44077  clsk1independent  44078  isotone1  44080  isotone2  44081  ntrclsiso  44099  ntrclsk2  44100  scottelrankd  44279  ssinc  45123  uzfissfz  45364  stoweidlem50  46087  stoweidlem57  46094  fourierdlem20  46164  fourierdlem50  46193  fourierdlem64  46207  fourierdlem86  46229  fourierdlem103  46246  fourierdlem104  46247  ovnval  46578  hoicvrrex  46593  ovnlecvr  46595  ovncvrrp  46601  ovnsubaddlem1  46607  hoidmvlelem3  46634  hoidmvle  46637  ovnhoilem1  46638  ovnhoi  46640  ovnlecvr2  46647  ovncvr2  46648  hspmbl  46666  ovolval4lem2  46687  ovolval5lem2  46690  ovolval5lem3  46691  ovolval5  46692  ovnovollem1  46693  ovnovollem2  46694  sprsymrelfvlem  47520  grlimedgclnbgr  48025  grlimgrtri  48033  grilcbri2  48041  uspgrsprf  48176  uspgrsprfo  48178  ssnn0ssfz  48379  lincfsuppcl  48444  iunlub  48851  lubeldm2d  48988  glbeldm2d  48989