Theorem sseq1d 4028

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq1d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq1 4022	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1538   ⊆ wss 3964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2728  df-ss 3981

This theorem is referenced by:  sseq12d  4030  eqsstrd  4035  ssiun2s  5054  disjxiun  5146  treq  5274  iunopeqop  5532  dfpo2  6321  preddowncl  6358  funimass1  6653  f1imadifssran  6657  feq1  6721  focofo  6838  fvmptss  7032  fvimacnvi  7076  fvimacnvALT  7081  knatar  7381  ovmptss  8123  fnsuppres  8221  frecseq123  8312  csbfrecsg  8314  frrlem1  8316  frrlem3  8318  frrlem4  8319  frrlem13  8328  frrdmcl  8338  fprresex  8340  wrecseq123OLD  8345  wfrlem1OLD  8353  wfrlem3OLD  8355  wfrdmclOLD  8362  wfrlem15OLD  8368  wfrlem17OLD  8370  dfrecs3  8417  dfrecs3OLD  8418  oaordi  8589  oaword2  8596  oawordeulem  8597  omword1  8616  oewordri  8635  oeordsuc  8637  nnaordi  8661  nnawordex  8680  naddcllem  8719  naddunif  8736  ereq1  8757  elpm2r  8890  inficl  9469  fipwss  9473  dffi3  9475  hartogslem1  9586  inf3lema  9668  inf3lemd  9671  cantnfle  9715  cantnflem2  9734  ttrclselem1  9769  trcl  9772  tcmin  9785  rankr1ai  9842  rankxplim  9923  scottex  9929  scott0  9930  scottexs  9931  scott0s  9932  karden  9939  cardne  10009  cardaleph  10133  ackbij2  10286  cflim2  10307  cfslb  10310  coftr  10317  fin23lem15  10378  fin23lem32  10388  fin23lem34  10390  fin23lem35  10391  fin23lem36  10392  fin23lem41  10396  isf32lem1  10397  itunitc1  10464  axdc3lem2  10495  ttukeylem1  10553  fpwwe2cbv  10674  fpwwe2lem2  10676  fpwwe2lem4  10678  fpwwe2  10687  fpwwecbv  10688  fpwwelem  10689  canthwelem  10694  canthwe  10695  pwfseqlem4  10706  wunex2  10782  wuncval2  10791  eltsk2g  10795  tskpwss  10796  inar1  10819  grothpw  10870  grothpwex  10871  axgroth6  10872  grothac  10874  peano5uzti  12712  fsuppmapnn0fiub0  14037  relexpnndm  15083  rtrclreclem4  15103  dfrtrcl2  15104  lo1o1  15571  o1lo1  15576  o1lo12  15577  lo1eq  15607  rlimeq  15608  isercoll  15707  prmreclem4  16959  vdwmc  17018  vdwlem1  17021  vdwlem2  17022  vdwlem12  17032  vdwlem13  17033  ramval  17048  ramz2  17064  ramub1lem1  17066  isacs2  17704  isacs1i  17708  mreacs  17709  acsfn  17710  rescabs  17889  rescabsOLD  17890  ipole  18598  ipodrsima  18605  isacs5  18612  symgsssg  19506  psgnunilem5  19533  sylow1  19642  efgval2  19763  efgsfo  19778  frgpuplem  19811  gsumzf1o  19951  gsumzoppg  19983  dprdcntz  20049  islbs2  21180  frlmssuvc1  21838  frlmssuvc2  21839  frlmsslsp  21840  ismhp  22168  pptbas  23037  pnfnei  23250  mnfnei  23251  iscnp  23267  iscnp4  23293  cnntr  23305  cnconst2  23313  cnpresti  23318  cnprest  23319  isreg  23362  isnrm  23365  isnrm2  23388  perfcls  23395  isreg2  23407  hauscmplem  23436  1stcfb  23475  1stcelcls  23491  1stccnp  23492  txbas  23597  ptbasfi  23611  xkoopn  23619  xkoccn  23649  txcnp  23650  ptcnplem  23651  txdis  23662  txdis1cn  23665  txtube  23670  txkgen  23682  xkohaus  23683  xkoptsub  23684  xkoco1cn  23687  xkoco2cn  23688  xkococnlem  23689  xkococn  23690  xkoinjcn  23717  kqreglem1  23771  kqreglem2  23772  kqnrmlem1  23773  kqnrmlem2  23774  reghmph  23823  nrmhmph  23824  trfil2  23917  ufileu  23949  elfm  23977  elfm2  23978  elfm3  23980  imaelfm  23981  rnelfm  23983  fmfnfmlem2  23985  fmfnfmlem4  23987  fmco  23991  elflim2  23994  flffbas  24025  lmflf  24035  txflf  24036  fclscf  24055  flimfnfcls  24058  cnextcn  24097  symgtgp  24136  ghmcnp  24145  qustgplem  24151  eltsms  24163  ustval  24233  ust0  24250  trust  24260  utoptop  24265  restutop  24268  restutopopn  24269  utopsnneiplem  24278  ucncn  24316  fmucnd  24323  cfilufg  24324  trcfilu  24325  neipcfilu  24327  blssps  24456  blss  24457  ssblex  24460  blin2  24461  metss2  24547  metrest  24559  metcnp3  24575  metustexhalf  24591  metustbl  24601  psmetutop  24602  xrsmopn  24856  recld2  24858  icccmplem1  24866  icccmplem2  24867  icccmp  24869  reconnlem2  24871  lebnumlem3  25017  lebnum  25018  xlebnum  25019  lebnumii  25020  nmhmcn  25175  cfilfval  25320  caubl  25364  caublcls  25365  bcthlem1  25380  bcth  25385  ovolfiniun  25558  ovoliunlem3  25561  ovoliun  25562  ovoliun2  25563  ovoliunnul  25564  voliunlem3  25609  dyadmax  25655  dyadmbllem  25656  dyadmbl  25657  opnmbllem  25658  ellimc2  25935  limcnlp  25936  ellimc3  25937  limcflf  25939  limciun  25952  cpnord  25994  lhop  26078  xrlimcnp  27034  cvxcl  27051  dchrval  27301  noetalem2  27810  madebdayim  27949  madebdaylemold  27959  madebday  27961  precsexlem8  28261  ausgrumgri  29207  ausgrusgri  29208  nbgrval  29376  nbgrel  29380  nbumgrvtx  29386  nbgrnself  29399  uvtxel1  29436  wlkonl1iedg  29706  crctcshwlkn0lem6  29858  2wlkdlem10  29978  1wlkdlem4  30182  3wlkdlem6  30207  3wlkdlem10  30211  eupth2lem3lem4  30273  frcond1  30308  frgr1v  30313  nfrgr2v  30314  frgr3vlem1  30315  frgr3vlem2  30316  frgr3v  30317  4cycl2vnunb  30332  n4cyclfrgr  30333  isssp  30766  ubthlem1  30912  shmodi  31432  chsupid  31454  chsscon3  31542  spansncvi  31694  mdslmd1lem3  32369  mdslmd1lem4  32370  mdsymlem5  32449  dmdbr5ati  32464  dmdbr6ati  32465  dmdbr7ati  32466  ssiun2sf  32593  fpwrelmapffslem  32763  pwrssmgc  32988  fldgenval  33307  unitprodclb  33410  resssra  33630  constrsscn  33758  txomap  33808  locfinreflem  33814  tpr2rico  33886  pnfneige0  33925  rrhre  33997  prodindf  34017  dya2icoseg2  34273  omsfval  34289  eulerpartlemt0  34364  eulerpartgbij  34367  eulerpartlemr  34369  eulerpartlemgs2  34375  eulerpartlemn  34376  eulerpart  34377  bnj517  34891  bnj1014  34967  bnj1015  34968  bnj1123  34992  bnj1125  34998  bnj1450  35056  bnj1452  35058  cplgredgex  35118  kur14  35213  cvmliftlem15  35295  cvmlift2lem12  35311  cvmlift2lem13  35312  mclsval  35560  mclsax  35566  mclsppslem  35580  prodeq12sdv  36213  cbvsumdavw2  36290  cbvproddavw2  36291  opnrebl  36315  opnrebl2  36316  ivthALT  36330  neibastop2lem  36355  fnemeet1  36361  filnetlem1  36373  filnetlem4  36376  bj-imdirval3  37179  bj-imdiridlem  37180  rdgssun  37373  lindsadd  37612  lindsenlbs  37614  ptrecube  37619  poimirlem32  37651  opnmbllem0  37655  mblfinlem1  37656  mblfinlem2  37657  mblfinlem3  37658  ovoliunnfl  37661  ex-ovoliunnfl  37662  voliunnfl  37663  totbndbnd  37788  heibor1lem  37808  heiborlem10  37819  scottexf  38167  scott0f  38168  relcnveq2  38317  cnvref4  38344  elrelscnveq2  38487  dfcnvrefrels2  38522  dfcnvrefrel2  38524  symrefref2  38557  lcv1  39035  lfl1dim  39115  lfl1dim2N  39116  paddasslem17  39831  dihglblem6  41335  dochvalr  41352  dochord3  41367  lpolconN  41482  lcfls1lem  41529  mapdffval  41621  mapdfval  41622  mapdsn2  41637  mapd0  41660  lspindp5  41765  mapdh8ab  41772  primrootscoprbij  42096  aks6d1c2  42124  aks6d1c6lem3  42166  aks6d1c6lem5  42171  aks6d1c7lem1  42174  ismrcd1  42700  nacsfix  42714  setindtr  43027  hbtlem6  43132  oaabsb  43298  tfsconcatrnss  43354  naddwordnexlem4  43405  clcnvlem  43627  iunrelexpmin1  43712  iunrelexpmin2  43716  relexp0a  43720  cotrcltrcl  43729  trclimalb2  43730  cotrclrcl  43746  sbcheg  43783  clsk1indlem1  44049  isotone1  44052  isotone2  44053  ntrclsiso  44071  ntrclsk2  44072  k0004lem1  44151  k0004lem3  44153  scottelrankd  44257  mnuop123d  44272  mnuprdlem1  44282  mnuprdlem2  44283  mnuunid  44287  mnurndlem1  44291  modelaxreplem1  44956  modelaxreplem2  44957  modelaxrep  44959  ssdec  45041  iinssd  45084  iinssdf  45092  ssnnf1octb  45149  iooiinicc  45507  iooiinioc  45521  icccncfext  45854  fourierdlem41  46115  meaiininclem  46453  hoidmvlelem3  46564  hoidmvle  46567  opnvonmbllem1  46599  opnvonmbl  46601  iinhoiicclem  46640  smflim  46744  smflimsuplem7  46793  clnbgrval  47758  clnbgrel  47764  sclnbgrel  47782  isubgredg  47801  isubgruhgr  47803  uhgrimisgrgriclem  47847  uhgrimisgrgric  47848  clnbgrgrimlem  47850  clnbgrgrim  47851  isubgr3stgrlem7  47888  uspgrlimlem1  47904  uspgrlimlem2  47905  uspgrlimlem3  47906  uspgrlim  47908  uspgrsprf  48011  iscnrm3r  48766  iscnrm3l  48769  setrecseq  48937  setrec1lem4  48942  setrec2fun  48944