Theorem sseq1d 3963

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sseq12d  3965  eqsstrd  3966  ssiun2s  4994  disjxiun  5085  treq  5202  iunopeqop  5458  dfpo2  6238  preddowncl  6274  funimass1  6558  f1imadifssran  6562  feq1  6624  focofo  6743  fvmptss  6935  fvimacnvi  6979  fvimacnvALT  6984  knatar  7285  ovmptss  8017  fnsuppres  8115  frecseq123  8206  csbfrecsg  8208  frrlem1  8210  frrlem3  8212  frrlem4  8213  frrlem13  8222  frrdmcl  8232  fprresex  8234  dfrecs3  8286  oaordi  8455  oaword2  8462  oawordeulem  8463  omword1  8482  oewordri  8501  oeordsuc  8503  nnaordi  8527  nnawordex  8546  naddcllem  8585  naddunif  8602  ereq1  8623  elpm2r  8763  inficl  9303  fipwss  9307  dffi3  9309  hartogslem1  9422  inf3lema  9508  inf3lemd  9511  cantnfle  9555  cantnflem2  9574  ttrclselem1  9609  trcl  9612  tcmin  9625  rankr1ai  9682  rankxplim  9763  scottex  9769  scott0  9770  scottexs  9771  scott0s  9772  karden  9779  cardne  9849  cardaleph  9971  ackbij2  10124  cflim2  10145  cfslb  10148  coftr  10155  fin23lem15  10216  fin23lem32  10226  fin23lem34  10228  fin23lem35  10229  fin23lem36  10230  fin23lem41  10234  isf32lem1  10235  itunitc1  10302  axdc3lem2  10333  ttukeylem1  10391  fpwwe2cbv  10512  fpwwe2lem2  10514  fpwwe2lem4  10516  fpwwe2  10525  fpwwecbv  10526  fpwwelem  10527  canthwelem  10532  canthwe  10533  pwfseqlem4  10544  wunex2  10620  wuncval2  10629  eltsk2g  10633  tskpwss  10634  inar1  10657  grothpw  10708  grothpwex  10709  axgroth6  10710  grothac  10712  peano5uzti  12554  fsuppmapnn0fiub0  13888  relexpnndm  14935  rtrclreclem4  14955  dfrtrcl2  14956  lo1o1  15426  o1lo1  15431  o1lo12  15432  lo1eq  15462  rlimeq  15463  isercoll  15562  prmreclem4  16818  vdwmc  16877  vdwlem1  16880  vdwlem2  16881  vdwlem12  16891  vdwlem13  16892  ramval  16907  ramz2  16923  ramub1lem1  16925  isacs2  17546  isacs1i  17550  mreacs  17551  acsfn  17552  rescabs  17727  ipole  18427  ipodrsima  18434  isacs5  18441  symgsssg  19333  psgnunilem5  19360  sylow1  19469  efgval2  19590  efgsfo  19605  frgpuplem  19638  gsumzf1o  19778  gsumzoppg  19810  dprdcntz  19876  islbs2  21045  frlmssuvc1  21685  frlmssuvc2  21686  frlmsslsp  21687  ismhp  22009  pptbas  22877  pnfnei  23089  mnfnei  23090  iscnp  23106  iscnp4  23132  cnntr  23144  cnconst2  23152  cnpresti  23157  cnprest  23158  isreg  23201  isnrm  23204  isnrm2  23227  perfcls  23234  isreg2  23246  hauscmplem  23275  1stcfb  23314  1stcelcls  23330  1stccnp  23331  txbas  23436  ptbasfi  23450  xkoopn  23458  xkoccn  23488  txcnp  23489  ptcnplem  23490  txdis  23501  txdis1cn  23504  txtube  23509  txkgen  23521  xkohaus  23522  xkoptsub  23523  xkoco1cn  23526  xkoco2cn  23527  xkococnlem  23528  xkococn  23529  xkoinjcn  23556  kqreglem1  23610  kqreglem2  23611  kqnrmlem1  23612  kqnrmlem2  23613  reghmph  23662  nrmhmph  23663  trfil2  23756  ufileu  23788  elfm  23816  elfm2  23817  elfm3  23819  imaelfm  23820  rnelfm  23822  fmfnfmlem2  23824  fmfnfmlem4  23826  fmco  23830  elflim2  23833  flffbas  23864  lmflf  23874  txflf  23875  fclscf  23894  flimfnfcls  23897  cnextcn  23936  symgtgp  23975  ghmcnp  23984  qustgplem  23990  eltsms  24002  ustval  24072  ust0  24089  trust  24098  utoptop  24103  restutop  24106  restutopopn  24107  utopsnneiplem  24116  ucncn  24153  fmucnd  24160  cfilufg  24161  trcfilu  24162  neipcfilu  24164  blssps  24293  blss  24294  ssblex  24297  blin2  24298  metss2  24381  metrest  24393  metcnp3  24409  metustexhalf  24425  metustbl  24435  psmetutop  24436  xrsmopn  24682  recld2  24684  icccmplem1  24692  icccmplem2  24693  icccmp  24695  reconnlem2  24697  lebnumlem3  24843  lebnum  24844  xlebnum  24845  lebnumii  24846  nmhmcn  25001  cfilfval  25145  caubl  25189  caublcls  25190  bcthlem1  25205  bcth  25210  ovolfiniun  25383  ovoliunlem3  25386  ovoliun  25387  ovoliun2  25388  ovoliunnul  25389  voliunlem3  25434  dyadmax  25480  dyadmbllem  25481  dyadmbl  25482  opnmbllem  25483  ellimc2  25759  limcnlp  25760  ellimc3  25761  limcflf  25763  limciun  25776  cpnord  25818  lhop  25902  xrlimcnp  26859  cvxcl  26876  dchrval  27126  noetalem2  27635  madebdayim  27787  madebdaylemold  27797  madebday  27799  bdayle  27815  precsexlem8  28106  ausgrumgri  29099  ausgrusgri  29100  nbgrval  29268  nbgrel  29272  nbumgrvtx  29278  nbgrnself  29291  uvtxel1  29328  wlkonl1iedg  29596  crctcshwlkn0lem6  29747  2wlkdlem10  29867  1wlkdlem4  30071  3wlkdlem6  30096  3wlkdlem10  30100  eupth2lem3lem4  30162  frcond1  30197  frgr1v  30202  nfrgr2v  30203  frgr3vlem1  30204  frgr3vlem2  30205  frgr3v  30206  4cycl2vnunb  30221  n4cyclfrgr  30222  isssp  30655  ubthlem1  30801  shmodi  31321  chsupid  31343  chsscon3  31431  spansncvi  31583  mdslmd1lem3  32258  mdslmd1lem4  32259  mdsymlem5  32338  dmdbr5ati  32353  dmdbr6ati  32354  dmdbr7ati  32355  ssiun2sf  32491  fpwrelmapffslem  32667  prodindf  32799  pwrssmgc  32937  fldgenval  33246  unitprodclb  33322  esplysply  33560  resssra  33567  constrsscn  33721  constrextdg2lem  33729  constrextdg2  33730  txomap  33815  locfinreflem  33821  tpr2rico  33893  pnfneige0  33932  rrhre  34002  dya2icoseg2  34259  omsfval  34275  eulerpartlemt0  34350  eulerpartgbij  34353  eulerpartlemr  34355  eulerpartlemgs2  34361  eulerpartlemn  34362  eulerpart  34363  bnj517  34865  bnj1014  34941  bnj1015  34942  bnj1123  34966  bnj1125  34972  bnj1450  35030  bnj1452  35032  cplgredgex  35111  kur14  35206  cvmliftlem15  35288  cvmlift2lem12  35304  cvmlift2lem13  35305  mclsval  35553  mclsax  35559  mclsppslem  35573  prodeq12sdv  36209  cbvsumdavw2  36286  cbvproddavw2  36287  opnrebl  36311  opnrebl2  36312  ivthALT  36326  neibastop2lem  36351  fnemeet1  36357  filnetlem1  36369  filnetlem4  36372  bj-imdirval3  37175  bj-imdiridlem  37176  rdgssun  37369  lindsadd  37610  lindsenlbs  37612  ptrecube  37617  poimirlem32  37649  opnmbllem0  37653  mblfinlem1  37654  mblfinlem2  37655  mblfinlem3  37656  ovoliunnfl  37659  ex-ovoliunnfl  37660  voliunnfl  37661  totbndbnd  37786  heibor1lem  37806  heiborlem10  37817  scottexf  38165  scott0f  38166  relcnveq2  38314  cnvref4  38335  elrelscnveq2  38487  dfcnvrefrels2  38522  dfcnvrefrel2  38524  symrefref2  38557  lcv1  39037  lfl1dim  39117  lfl1dim2N  39118  paddasslem17  39832  dihglblem6  41336  dochvalr  41353  dochord3  41368  lpolconN  41483  lcfls1lem  41530  mapdffval  41622  mapdfval  41623  mapdsn2  41638  mapd0  41661  lspindp5  41766  mapdh8ab  41773  primrootscoprbij  42092  aks6d1c2  42120  aks6d1c6lem3  42162  aks6d1c6lem5  42167  aks6d1c7lem1  42170  ismrcd1  42688  nacsfix  42702  setindtr  43014  hbtlem6  43119  oaabsb  43284  tfsconcatrnss  43340  naddwordnexlem4  43391  clcnvlem  43613  iunrelexpmin1  43698  iunrelexpmin2  43702  relexp0a  43706  cotrcltrcl  43715  trclimalb2  43716  cotrclrcl  43732  sbcheg  43769  clsk1indlem1  44035  isotone1  44038  isotone2  44039  ntrclsiso  44057  ntrclsk2  44058  k0004lem1  44137  k0004lem3  44139  scottelrankd  44237  mnuop123d  44252  mnuprdlem1  44262  mnuprdlem2  44263  mnuunid  44267  mnurndlem1  44271  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  ssdec  45082  iinssd  45125  iinssdf  45133  ssnnf1octb  45188  iooiinicc  45539  iooiinioc  45553  icccncfext  45882  fourierdlem41  46143  meaiininclem  46481  hoidmvlelem3  46592  hoidmvle  46595  opnvonmbllem1  46627  opnvonmbl  46629  iinhoiicclem  46668  smflim  46772  smflimsuplem7  46821  clnbgrval  47820  clnbgrel  47826  sclnbgrel  47845  isubgredg  47864  isubgruhgr  47866  uhgrimisgrgriclem  47928  uhgrimisgrgric  47929  clnbgrgrimlem  47931  clnbgrgrim  47932  isubgr3stgrlem7  47970  uspgrlimlem1  47986  uspgrlimlem2  47987  uspgrlimlem3  47988  uspgrlim  47990  pgnbgreunbgr  48123  uspgrsprf  48144  iinglb  48820  iscnrm3r  48946  iscnrm3l  48949  imassc  49152  setrecseq  49684  setrec1lem4  49689  setrec2fun  49691