Theorem sseq1d 3944

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  sseq12d  3946  eqsstrd  3947  ssiun2s  5010  disjxiun  5103  treq  5222  iunopeqop  5498  iunopeqopOLD  5499  dfpo2  6317  preddowncl  6353  funimass1  6644  feq1  6709  focofo  6831  fvmptss  7029  fvimacnvi  7074  fvimacnvALT  7079  knatar  7390  ovmptssOLD  8130  fnsuppres  8236  frecseq123  8328  csbfrecsg  8330  frrlem1  8332  frrlem3  8334  frrlem4  8335  frrlem13  8344  frrdmcl  8354  fprresex  8356  dfrecs3  8408  oaordi  8582  oaword2  8589  oawordeulem  8590  omword1  8609  oewordri  8629  oeordsuc  8631  nnaordi  8655  nnawordex  8674  naddcllem  8713  naddunif  8731  ereq1  8753  elpm2r  8893  inficl  9444  fipwss  9448  dffi3  9450  hartogslem1  9563  inf3lema  9652  inf3lemd  9655  cantnfle  9699  cantnflem2  9718  ttrclselem1  9753  trcl  9756  tcmin  9767  rankr1ai  9833  rankxplim  9923  scottex  9960  scottexOLD  9961  scott0b  9964  scott0OLD  9965  scottexsOLD  9970  scott0bsOLD  9972  scottelrankd  9975  kardenOLD  9987  setrec1lem4  9998  setrec2fun  10000  cardne  10073  cardaleph  10195  ackbij2  10347  cflim2  10368  cfslb  10371  coftr  10378  fin23lem15  10439  fin23lem32  10449  fin23lem34  10451  fin23lem35  10452  fin23lem36  10453  fin23lem41  10457  isf32lem1  10458  itunitc1  10525  axdc3lem2  10556  ttukeylem1  10614  fpwwe2cbv  10742  fpwwe2lem2  10744  fpwwe2lem4  10746  fpwwe2  10755  fpwwecbv  10756  fpwwelem  10757  canthwelem  10762  canthwe  10763  pwfseqlem4  10774  wunex2  10850  wuncval2  10859  eltsk2g  10863  tskpwss  10864  inar1  10887  grothpw  10938  grothpwex  10939  axgroth6  10940  grothac  10942  peano5uzti  12816  fsuppmapnn0fiub0  14163  relexpnndm  15223  rtrclreclem4  15243  dfrtrcl2  15244  lo1o1  15728  o1lo1  15733  o1lo12  15734  lo1eq  15764  rlimeq  15765  isercoll  15864  prmreclem4  17126  vdwmc  17185  vdwlem1  17188  vdwlem2  17189  vdwlem12  17199  vdwlem13  17200  ramval  17215  ramz2  17231  ramub1lem1  17233  isacs2  17856  isacs1i  17860  mreacs  17861  acsfn  17862  rescabs  18037  ipole  18737  ipodrsima  18744  isacs5  18751  symgsssg  19711  psgnunilem5  19738  sylow1  19847  efgval2  19968  efgsfo  19983  frgpuplem  20016  gsumzf1o  20156  gsumzoppg  20188  dprdcntz  20254  islbs2  21462  frlmssuvc1  22130  frlmssuvc2  22131  frlmsslsp  22132  lindsenlbs  22187  ismhp  22491  pptbas  23356  pnfnei  23568  mnfnei  23569  iscnp  23585  iscnp4  23611  cnntr  23623  cnconst2  23631  cnpresti  23636  cnprest  23637  isreg  23680  isnrm  23683  isnrm2  23706  perfcls  23713  isreg2  23725  hauscmplem  23754  1stcfb  23793  1stcelcls  23810  1stccnp  23811  txbas  23916  ptbasfi  23930  xkoopn  23938  xkoccn  23968  txcnp  23969  ptcnplem  23970  txdis  23981  txdis1cn  23984  txtube  23989  txkgen  24001  xkohaus  24002  xkoptsub  24003  xkoco1cn  24006  xkoco2cn  24007  xkococnlem  24008  xkococn  24009  xkoinjcn  24036  kqreglem1  24090  kqreglem2  24091  kqnrmlem1  24092  kqnrmlem2  24093  reghmph  24142  nrmhmph  24143  trfil2  24236  ufileu  24268  elfm  24296  elfm2  24297  elfm3  24299  imaelfm  24300  rnelfm  24302  fmfnfmlem2  24304  fmfnfmlem4  24306  fmco  24310  elflim2  24313  flffbas  24344  lmflf  24354  txflf  24355  fclscf  24374  flimfnfcls  24377  cnextcn  24416  symgtgp  24455  ghmcnp  24464  qustgplem  24470  eltsms  24482  ustval  24552  ust0  24569  trust  24578  utoptop  24583  restutop  24586  restutopopn  24587  utopsnneiplem  24596  ucncn  24633  fmucnd  24640  cfilufg  24641  trcfilu  24642  neipcfilu  24644  blssps  24773  blss  24774  ssblex  24777  blin2  24778  metss2  24861  metrest  24873  metcnp3  24889  metustexhalf  24905  metustbl  24915  psmetutop  24916  xrsmopn  25162  recld2  25164  icccmplem1  25172  icccmplem2  25173  icccmp  25175  reconnlem2  25177  lebnumlem3  25314  lebnum  25315  xlebnum  25316  lebnumii  25317  nmhmcn  25471  cfilfval  25615  caubl  25659  caublcls  25660  bcthlem1  25675  bcth  25680  ovolfiniun  25852  ovoliunlem3  25855  ovoliun  25856  ovoliun2  25857  ovoliunnul  25858  voliunlem3  25903  dyadmax  25949  dyadmbllem  25950  dyadmbl  25951  opnmbllem  25952  ellimc2  26227  limcnlp  26228  ellimc3  26229  limcflf  26231  limciun  26244  cpnord  26285  lhop  26366  xrlimcnp  27326  cvxcl  27342  dchrval  27591  noetalem2  28129  madebdayim  28304  madebdaylemold  28314  madebday  28316  bdayle  28332  precsexlem8  28630  bdaypw2n0bndlem  28879  bdayfinbndcbv  28882  bdayfinbndlem1  28883  bdayfinbndlem2  28884  bdayfinbnd  28885  lnssplng  29300  ausgrumgri  29778  ausgrusgri  29779  nbgrval  29947  nbgrel  29951  nbumgrvtx  29957  nbgrnself  29970  uvtxel1  30007  wlkonl1iedg  30274  crctcshwlkn0lem6  30434  2wlkdlem10  30554  1wlkdlem4  30761  3wlkdlem6  30796  3wlkdlem10  30800  eupth2lem3lem4  30862  frcond1  30897  frgr1v  30902  nfrgr2v  30903  frgr3vlem1  30904  frgr3vlem2  30905  frgr3v  30906  4cycl2vnunb  30921  n4cyclfrgr  30922  isssp  31356  ubthlem1  31502  shmodi  32022  chsupid  32044  chsscon3  32132  spansncvi  32284  mdslmd1lem3  32959  mdslmd1lem4  32960  mdsymlem5  33039  dmdbr5ati  33054  dmdbr6ati  33055  dmdbr7ati  33056  ssiun2sf  33226  fpwrelmapffslem  33394  prodindf  33499  pwrssmgc  33631  fldgenval  33944  unitprodclb  34014  esplysply  34273  esplyfvaln  34276  esplyind  34277  resssra  34289  constrsscn  34442  constrextdg2lem  34450  constrextdg2  34451  txomap  34536  locfinreflem  34542  tpr2rico  34614  pnfneige0  34653  rrhre  34723  dya2icoseg2  34980  omsfval  34996  eulerpartlemt0  35071  eulerpartgbij  35074  eulerpartlemr  35076  eulerpartlemgs2  35082  eulerpartlemn  35083  eulerpart  35084  bnj517  35585  bnj1014  35661  bnj1015  35662  bnj1123  35686  bnj1125  35692  bnj1450  35750  bnj1452  35752  rankse  35823  elscott  35825  elkarden  35923  cplgredgex  36062  kur14  36148  cvmliftlem15  36230  cvmlift2lem12  36246  cvmlift2lem13  36247  mclsval  36495  mclsax  36501  mclsppslem  36515  prodeq12sdv  37185  cbvsumdavw2  37262  cbvproddavw2  37263  opnrebl  37286  opnrebl2  37287  ivthALT  37301  neibastop2lem  37326  fnemeet1  37332  filnetlem1  37344  filnetlem4  37347  ttcmin  37462  dfttc2g  37472  resssres  38139  bj-imdirval3  38297  bj-imdiridlem  38298  rdgssun  38493  lindsadd  38728  ptrecube  38730  poimirlem32  38762  opnmbllem0  38766  mblfinlem1  38767  mblfinlem2  38768  mblfinlem3  38769  ovoliunnfl  38772  ex-ovoliunnfl  38773  voliunnfl  38774  totbndbnd  38915  heibor1lem  38935  heiborlem10  38946  scottexf  39292  scott0f  39293  relcnveq2  39453  cnvref4  39474  dfcnvrefrels2  39732  dfcnvrefrel2  39734  elrelscnveq2  39753  symrefref2  39771  lcv1  40290  lfl1dim  40370  lfl1dim2N  40371  paddasslem17  41085  dihglblem6  42589  dochvalr  42606  dochord3  42621  lpolconN  42736  lcfls1lem  42783  mapdffval  42875  mapdfval  42876  mapdsn2  42891  mapd0  42914  lspindp5  43019  mapdh8ab  43026  primrootscoprbij  43344  aks6d1c2  43372  aks6d1c6lem3  43414  aks6d1c6lem5  43419  aks6d1c7lem1  43422  ismrcd1  43902  nacsfix  43916  setindtr  44224  hbtlem6  44323  oaabsb  44488  tfsconcatrnss  44544  naddwordnexlem4  44595  clcnvlem  44815  iunrelexpmin1  44900  iunrelexpmin2  44904  relexp0a  44908  cotrcltrcl  44917  trclimalb2  44918  cotrclrcl  44934  sbcheg  44971  clsk1indlem1  45237  isotone1  45240  isotone2  45241  ntrclsiso  45259  ntrclsk2  45260  k0004lem1  45339  k0004lem3  45341  mnuop123d  45438  mnuprdlem1  45448  mnuprdlem2  45449  mnuunid  45453  mnurndlem1  45457  modelaxreplem1  46163  modelaxreplem2  46164  modelaxrep  46166  ssdec  46308  iinssd  46351  iinssdf  46359  ssnnf1octb  46414  iooiinicc  46759  iooiinioc  46773  icccncfext  47102  fourierdlem41  47363  meaiininclem  47701  hoidmvlelem3  47812  hoidmvle  47815  opnvonmbllem1  47847  opnvonmbl  47849  iinhoiicclem  47888  smflim  47992  smflimsuplem7  48041  clnbgrval  49125  clnbgrel  49131  sclnbgrel  49150  isubgredg  49169  isubgruhgr  49171  uhgrimisgrgriclem  49233  uhgrimisgrgric  49234  clnbgrgrimlem  49236  clnbgrgrim  49237  isubgr3stgrlem7  49275  uspgrlimlem1  49291  uspgrlimlem2  49292  uspgrlimlem3  49293  uspgrlim  49295  pgnbgreunbgr  49428  uspgrsprf  49449  iinglb  50138  iscnrm3r  50267  iscnrm3l  50270  imassc  50474  setrecseq  51068