Theorem sseq1d 3954

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseq12d  3956  eqsstrd  3957  ssiun2s  4992  disjxiun  5083  treq  5200  iunopeqop  5469  dfpo2  6254  preddowncl  6290  funimass1  6574  f1imadifssran  6578  feq1  6640  focofo  6759  fvmptss  6954  fvimacnvi  6998  fvimacnvALT  7003  knatar  7305  ovmptss  8036  fnsuppres  8134  frecseq123  8225  csbfrecsg  8227  frrlem1  8229  frrlem3  8231  frrlem4  8232  frrlem13  8241  frrdmcl  8251  fprresex  8253  dfrecs3  8305  oaordi  8474  oaword2  8481  oawordeulem  8482  omword1  8501  oewordri  8521  oeordsuc  8523  nnaordi  8547  nnawordex  8566  naddcllem  8605  naddunif  8622  ereq1  8644  elpm2r  8785  inficl  9331  fipwss  9335  dffi3  9337  hartogslem1  9450  inf3lema  9536  inf3lemd  9539  cantnfle  9583  cantnflem2  9602  ttrclselem1  9637  trcl  9640  tcmin  9651  rankr1ai  9713  rankxplim  9794  scottex  9800  scott0  9801  scottexs  9802  scott0s  9803  karden  9810  cardne  9880  cardaleph  10002  ackbij2  10155  cflim2  10176  cfslb  10179  coftr  10186  fin23lem15  10247  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem36  10261  fin23lem41  10265  isf32lem1  10266  itunitc1  10333  axdc3lem2  10364  ttukeylem1  10422  fpwwe2cbv  10544  fpwwe2lem2  10546  fpwwe2lem4  10548  fpwwe2  10557  fpwwecbv  10558  fpwwelem  10559  canthwelem  10564  canthwe  10565  pwfseqlem4  10576  wunex2  10652  wuncval2  10661  eltsk2g  10665  tskpwss  10666  inar1  10689  grothpw  10740  grothpwex  10741  axgroth6  10742  grothac  10744  peano5uzti  12610  fsuppmapnn0fiub0  13946  relexpnndm  14994  rtrclreclem4  15014  dfrtrcl2  15015  lo1o1  15485  o1lo1  15490  o1lo12  15491  lo1eq  15521  rlimeq  15522  isercoll  15621  prmreclem4  16881  vdwmc  16940  vdwlem1  16943  vdwlem2  16944  vdwlem12  16954  vdwlem13  16955  ramval  16970  ramz2  16986  ramub1lem1  16988  isacs2  17610  isacs1i  17614  mreacs  17615  acsfn  17616  rescabs  17791  ipole  18491  ipodrsima  18498  isacs5  18505  symgsssg  19433  psgnunilem5  19460  sylow1  19569  efgval2  19690  efgsfo  19705  frgpuplem  19738  gsumzf1o  19878  gsumzoppg  19910  dprdcntz  19976  islbs2  21144  frlmssuvc1  21784  frlmssuvc2  21785  frlmsslsp  21786  ismhp  22116  pptbas  22983  pnfnei  23195  mnfnei  23196  iscnp  23212  iscnp4  23238  cnntr  23250  cnconst2  23258  cnpresti  23263  cnprest  23264  isreg  23307  isnrm  23310  isnrm2  23333  perfcls  23340  isreg2  23352  hauscmplem  23381  1stcfb  23420  1stcelcls  23436  1stccnp  23437  txbas  23542  ptbasfi  23556  xkoopn  23564  xkoccn  23594  txcnp  23595  ptcnplem  23596  txdis  23607  txdis1cn  23610  txtube  23615  txkgen  23627  xkohaus  23628  xkoptsub  23629  xkoco1cn  23632  xkoco2cn  23633  xkococnlem  23634  xkococn  23635  xkoinjcn  23662  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  reghmph  23768  nrmhmph  23769  trfil2  23862  ufileu  23894  elfm  23922  elfm2  23923  elfm3  23925  imaelfm  23926  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  fmco  23936  elflim2  23939  flffbas  23970  lmflf  23980  txflf  23981  fclscf  24000  flimfnfcls  24003  cnextcn  24042  symgtgp  24081  ghmcnp  24090  qustgplem  24096  eltsms  24108  ustval  24178  ust0  24195  trust  24204  utoptop  24209  restutop  24212  restutopopn  24213  utopsnneiplem  24222  ucncn  24259  fmucnd  24266  cfilufg  24267  trcfilu  24268  neipcfilu  24270  blssps  24399  blss  24400  ssblex  24403  blin2  24404  metss2  24487  metrest  24499  metcnp3  24515  metustexhalf  24531  metustbl  24541  psmetutop  24542  xrsmopn  24788  recld2  24790  icccmplem1  24798  icccmplem2  24799  icccmp  24801  reconnlem2  24803  lebnumlem3  24940  lebnum  24941  xlebnum  24942  lebnumii  24943  nmhmcn  25097  cfilfval  25241  caubl  25285  caublcls  25286  bcthlem1  25301  bcth  25306  ovolfiniun  25478  ovoliunlem3  25481  ovoliun  25482  ovoliun2  25483  ovoliunnul  25484  voliunlem3  25529  dyadmax  25575  dyadmbllem  25576  dyadmbl  25577  opnmbllem  25578  ellimc2  25854  limcnlp  25855  ellimc3  25856  limcflf  25858  limciun  25871  cpnord  25912  lhop  25993  xrlimcnp  26945  cvxcl  26962  dchrval  27211  noetalem2  27720  madebdayim  27894  madebdaylemold  27904  madebday  27906  bdayle  27922  precsexlem8  28220  bdaypw2n0bndlem  28469  bdayfinbndcbv  28472  bdayfinbndlem1  28473  bdayfinbndlem2  28474  bdayfinbnd  28475  ausgrumgri  29250  ausgrusgri  29251  nbgrval  29419  nbgrel  29423  nbumgrvtx  29429  nbgrnself  29442  uvtxel1  29479  wlkonl1iedg  29747  crctcshwlkn0lem6  29898  2wlkdlem10  30018  1wlkdlem4  30225  3wlkdlem6  30250  3wlkdlem10  30254  eupth2lem3lem4  30316  frcond1  30351  frgr1v  30356  nfrgr2v  30357  frgr3vlem1  30358  frgr3vlem2  30359  frgr3v  30360  4cycl2vnunb  30375  n4cyclfrgr  30376  isssp  30810  ubthlem1  30956  shmodi  31476  chsupid  31498  chsscon3  31586  spansncvi  31738  mdslmd1lem3  32413  mdslmd1lem4  32414  mdsymlem5  32493  dmdbr5ati  32508  dmdbr6ati  32509  dmdbr7ati  32510  ssiun2sf  32644  fpwrelmapffslem  32820  prodindf  32937  pwrssmgc  33075  fldgenval  33388  unitprodclb  33464  esplysply  33730  esplyfvaln  33733  esplyind  33734  resssra  33746  constrsscn  33900  constrextdg2lem  33908  constrextdg2  33909  txomap  33994  locfinreflem  34000  tpr2rico  34072  pnfneige0  34111  rrhre  34181  dya2icoseg2  34438  omsfval  34454  eulerpartlemt0  34529  eulerpartgbij  34532  eulerpartlemr  34534  eulerpartlemgs2  34540  eulerpartlemn  34541  eulerpart  34542  bnj517  35043  bnj1014  35119  bnj1015  35120  bnj1123  35144  bnj1125  35150  bnj1450  35208  bnj1452  35210  cplgredgex  35319  kur14  35414  cvmliftlem15  35496  cvmlift2lem12  35512  cvmlift2lem13  35513  mclsval  35761  mclsax  35767  mclsppslem  35781  prodeq12sdv  36416  cbvsumdavw2  36493  cbvproddavw2  36494  opnrebl  36518  opnrebl2  36519  ivthALT  36533  neibastop2lem  36558  fnemeet1  36564  filnetlem1  36576  filnetlem4  36579  ttcmin  36694  dfttc2g  36704  bj-imdirval3  37514  bj-imdiridlem  37515  rdgssun  37708  lindsadd  37948  lindsenlbs  37950  ptrecube  37955  poimirlem32  37987  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  ovoliunnfl  37997  ex-ovoliunnfl  37998  voliunnfl  37999  totbndbnd  38124  heibor1lem  38144  heiborlem10  38155  scottexf  38503  scott0f  38504  relcnveq2  38664  cnvref4  38685  dfcnvrefrels2  38943  dfcnvrefrel2  38945  elrelscnveq2  38964  symrefref2  38982  lcv1  39501  lfl1dim  39581  lfl1dim2N  39582  paddasslem17  40296  dihglblem6  41800  dochvalr  41817  dochord3  41832  lpolconN  41947  lcfls1lem  41994  mapdffval  42086  mapdfval  42087  mapdsn2  42102  mapd0  42125  lspindp5  42230  mapdh8ab  42237  primrootscoprbij  42555  aks6d1c2  42583  aks6d1c6lem3  42625  aks6d1c6lem5  42630  aks6d1c7lem1  42633  ismrcd1  43144  nacsfix  43158  setindtr  43470  hbtlem6  43575  oaabsb  43740  tfsconcatrnss  43796  naddwordnexlem4  43847  clcnvlem  44068  iunrelexpmin1  44153  iunrelexpmin2  44157  relexp0a  44161  cotrcltrcl  44170  trclimalb2  44171  cotrclrcl  44187  sbcheg  44224  clsk1indlem1  44490  isotone1  44493  isotone2  44494  ntrclsiso  44512  ntrclsk2  44513  k0004lem1  44592  k0004lem3  44594  scottelrankd  44692  mnuop123d  44707  mnuprdlem1  44717  mnuprdlem2  44718  mnuunid  44722  mnurndlem1  44726  modelaxreplem1  45423  modelaxreplem2  45424  modelaxrep  45426  ssdec  45536  iinssd  45579  iinssdf  45587  ssnnf1octb  45642  iooiinicc  45990  iooiinioc  46004  icccncfext  46333  fourierdlem41  46594  meaiininclem  46932  hoidmvlelem3  47043  hoidmvle  47046  opnvonmbllem1  47078  opnvonmbl  47080  iinhoiicclem  47119  smflim  47223  smflimsuplem7  47272  clnbgrval  48310  clnbgrel  48316  sclnbgrel  48335  isubgredg  48354  isubgruhgr  48356  uhgrimisgrgriclem  48418  uhgrimisgrgric  48419  clnbgrgrimlem  48421  clnbgrgrim  48422  isubgr3stgrlem7  48460  uspgrlimlem1  48476  uspgrlimlem2  48477  uspgrlimlem3  48478  uspgrlim  48480  pgnbgreunbgr  48613  uspgrsprf  48634  iinglb  49309  iscnrm3r  49435  iscnrm3l  49438  imassc  49640  setrecseq  50172  setrec1lem4  50177  setrec2fun  50179