Theorem sseq1d 3968

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is used by:  sseq12d  3970  eqsstrd  3971  ssiun2s  5013  disjxiun  5106  treq  5225  iunopeqop  5504  iunopeqopOLD  5505  dfpo2  6297  preddowncl  6333  funimass1  6618  feq1  6683  focofo  6805  fvmptss  7002  fvimacnvi  7047  fvimacnvALT  7052  knatar  7355  ovmptss  8084  fnsuppres  8183  frecseq123  8275  csbfrecsg  8277  frrlem1  8279  frrlem3  8281  frrlem4  8282  frrlem13  8291  frrdmcl  8301  fprresex  8303  dfrecs3  8355  oaordi  8527  oaword2  8534  oawordeulem  8535  omword1  8554  oewordri  8574  oeordsuc  8576  nnaordi  8600  nnawordex  8619  naddcllem  8658  naddunif  8676  ereq1  8698  elpm2r  8838  inficl  9381  fipwss  9385  dffi3  9387  hartogslem1  9500  inf3lema  9589  inf3lemd  9592  cantnfle  9636  cantnflem2  9655  ttrclselem1  9690  trcl  9693  tcmin  9704  rankr1ai  9766  rankxplim  9847  scottex  9858  scottexOLD  9859  scott0b  9862  scott0OLD  9863  scottexsOLD  9868  scott0bsOLD  9870  scottelrankd  9873  kardenOLD  9885  cardne  9956  cardaleph  10078  ackbij2  10230  cflim2  10251  cfslb  10254  coftr  10261  fin23lem15  10322  fin23lem32  10332  fin23lem34  10334  fin23lem35  10335  fin23lem36  10336  fin23lem41  10340  isf32lem1  10341  itunitc1  10408  axdc3lem2  10439  ttukeylem1  10497  fpwwe2cbv  10619  fpwwe2lem2  10621  fpwwe2lem4  10623  fpwwe2  10632  fpwwecbv  10633  fpwwelem  10634  canthwelem  10639  canthwe  10640  pwfseqlem4  10651  wunex2  10727  wuncval2  10736  eltsk2g  10740  tskpwss  10741  inar1  10764  grothpw  10815  grothpwex  10816  axgroth6  10817  grothac  10819  peano5uzti  12690  fsuppmapnn0fiub0  14034  relexpnndm  15083  rtrclreclem4  15103  dfrtrcl2  15104  lo1o1  15588  o1lo1  15593  o1lo12  15594  lo1eq  15624  rlimeq  15625  isercoll  15724  prmreclem4  16983  vdwmc  17042  vdwlem1  17045  vdwlem2  17046  vdwlem12  17056  vdwlem13  17057  ramval  17072  ramz2  17088  ramub1lem1  17090  isacs2  17713  isacs1i  17717  mreacs  17718  acsfn  17719  rescabs  17894  ipole  18594  ipodrsima  18601  isacs5  18608  symgsssg  19541  psgnunilem5  19568  sylow1  19677  efgval2  19798  efgsfo  19813  frgpuplem  19846  gsumzf1o  19986  gsumzoppg  20018  dprdcntz  20084  islbs2  21287  frlmssuvc1  21953  frlmssuvc2  21954  frlmsslsp  21955  ismhp  22312  pptbas  23174  pnfnei  23386  mnfnei  23387  iscnp  23403  iscnp4  23429  cnntr  23441  cnconst2  23449  cnpresti  23454  cnprest  23455  isreg  23498  isnrm  23501  isnrm2  23524  perfcls  23531  isreg2  23543  hauscmplem  23572  1stcfb  23611  1stcelcls  23627  1stccnp  23628  txbas  23733  ptbasfi  23747  xkoopn  23755  xkoccn  23785  txcnp  23786  ptcnplem  23787  txdis  23798  txdis1cn  23801  txtube  23806  txkgen  23818  xkohaus  23819  xkoptsub  23820  xkoco1cn  23823  xkoco2cn  23824  xkococnlem  23825  xkococn  23826  xkoinjcn  23853  kqreglem1  23907  kqreglem2  23908  kqnrmlem1  23909  kqnrmlem2  23910  reghmph  23959  nrmhmph  23960  trfil2  24053  ufileu  24085  elfm  24113  elfm2  24114  elfm3  24116  imaelfm  24117  rnelfm  24119  fmfnfmlem2  24121  fmfnfmlem4  24123  fmco  24127  elflim2  24130  flffbas  24161  lmflf  24171  txflf  24172  fclscf  24191  flimfnfcls  24194  cnextcn  24233  symgtgp  24272  ghmcnp  24281  qustgplem  24287  eltsms  24299  ustval  24369  ust0  24386  trust  24395  utoptop  24400  restutop  24403  restutopopn  24404  utopsnneiplem  24413  ucncn  24450  fmucnd  24457  cfilufg  24458  trcfilu  24459  neipcfilu  24461  blssps  24590  blss  24591  ssblex  24594  blin2  24595  metss2  24678  metrest  24690  metcnp3  24706  metustexhalf  24722  metustbl  24732  psmetutop  24733  xrsmopn  24979  recld2  24981  icccmplem1  24989  icccmplem2  24990  icccmp  24992  reconnlem2  24994  lebnumlem3  25131  lebnum  25132  xlebnum  25133  lebnumii  25134  nmhmcn  25288  cfilfval  25432  caubl  25476  caublcls  25477  bcthlem1  25492  bcth  25497  ovolfiniun  25669  ovoliunlem3  25672  ovoliun  25673  ovoliun2  25674  ovoliunnul  25675  voliunlem3  25720  dyadmax  25766  dyadmbllem  25767  dyadmbl  25768  opnmbllem  25769  ellimc2  26045  limcnlp  26046  ellimc3  26047  limcflf  26049  limciun  26062  cpnord  26103  lhop  26184  xrlimcnp  27142  cvxcl  27158  dchrval  27407  noetalem2  27915  madebdayim  28090  madebdaylemold  28100  madebday  28102  bdayle  28118  precsexlem8  28416  bdaypw2n0bndlem  28665  bdayfinbndcbv  28668  bdayfinbndlem1  28669  bdayfinbndlem2  28670  bdayfinbnd  28671  lnssplng  29083  ausgrumgri  29526  ausgrusgri  29527  nbgrval  29695  nbgrel  29699  nbumgrvtx  29705  nbgrnself  29718  uvtxel1  29755  wlkonl1iedg  30022  crctcshwlkn0lem6  30173  2wlkdlem10  30293  1wlkdlem4  30500  3wlkdlem6  30525  3wlkdlem10  30529  eupth2lem3lem4  30591  frcond1  30626  frgr1v  30631  nfrgr2v  30632  frgr3vlem1  30633  frgr3vlem2  30634  frgr3v  30635  4cycl2vnunb  30650  n4cyclfrgr  30651  isssp  31085  ubthlem1  31231  shmodi  31751  chsupid  31773  chsscon3  31861  spansncvi  32013  mdslmd1lem3  32688  mdslmd1lem4  32689  mdsymlem5  32768  dmdbr5ati  32783  dmdbr6ati  32784  dmdbr7ati  32785  ssiun2sf  32913  fpwrelmapffslem  33086  prodindf  33191  pwrssmgc  33329  fldgenval  33642  unitprodclb  33711  esplysply  33970  esplyfvaln  33973  esplyind  33974  resssra  33986  constrsscn  34139  constrextdg2lem  34147  constrextdg2  34148  txomap  34233  locfinreflem  34239  tpr2rico  34311  pnfneige0  34350  rrhre  34420  dya2icoseg2  34677  omsfval  34693  eulerpartlemt0  34768  eulerpartgbij  34771  eulerpartlemr  34773  eulerpartlemgs2  34779  eulerpartlemn  34780  eulerpart  34781  bnj517  35282  bnj1014  35358  bnj1015  35359  bnj1123  35383  bnj1125  35389  bnj1450  35447  bnj1452  35449  elscott  35519  elkarden  35576  cplgredgex  35621  kur14  35716  cvmliftlem15  35798  cvmlift2lem12  35814  cvmlift2lem13  35815  mclsval  36063  mclsax  36069  mclsppslem  36083  prodeq12sdv  36758  cbvsumdavw2  36835  cbvproddavw2  36836  opnrebl  36859  opnrebl2  36860  ivthALT  36874  neibastop2lem  36899  fnemeet1  36905  filnetlem1  36917  filnetlem4  36920  ttcmin  37035  dfttc2g  37045  bj-imdirval3  37856  bj-imdiridlem  37857  rdgssun  38052  lindsadd  38292  lindsenlbs  38294  ptrecube  38299  poimirlem32  38331  opnmbllem0  38335  mblfinlem1  38336  mblfinlem2  38337  mblfinlem3  38338  ovoliunnfl  38341  ex-ovoliunnfl  38342  voliunnfl  38343  totbndbnd  38468  heibor1lem  38488  heiborlem10  38499  scottexf  38845  scott0f  38846  relcnveq2  39006  cnvref4  39027  dfcnvrefrels2  39285  dfcnvrefrel2  39287  elrelscnveq2  39306  symrefref2  39324  lcv1  39843  lfl1dim  39923  lfl1dim2N  39924  paddasslem17  40638  dihglblem6  42142  dochvalr  42159  dochord3  42174  lpolconN  42289  lcfls1lem  42336  mapdffval  42428  mapdfval  42429  mapdsn2  42444  mapd0  42467  lspindp5  42572  mapdh8ab  42579  primrootscoprbij  42897  aks6d1c2  42925  aks6d1c6lem3  42967  aks6d1c6lem5  42972  aks6d1c7lem1  42975  ismrcd1  43457  nacsfix  43471  setindtr  43779  hbtlem6  43884  oaabsb  44049  tfsconcatrnss  44105  naddwordnexlem4  44156  clcnvlem  44377  iunrelexpmin1  44462  iunrelexpmin2  44466  relexp0a  44470  cotrcltrcl  44479  trclimalb2  44480  cotrclrcl  44496  sbcheg  44533  clsk1indlem1  44799  isotone1  44802  isotone2  44803  ntrclsiso  44821  ntrclsk2  44822  k0004lem1  44901  k0004lem3  44903  mnuop123d  45000  mnuprdlem1  45010  mnuprdlem2  45011  mnuunid  45015  mnurndlem1  45019  modelaxreplem1  45715  modelaxreplem2  45716  modelaxrep  45718  ssdec  45834  iinssd  45877  iinssdf  45885  ssnnf1octb  45940  iooiinicc  46286  iooiinioc  46300  icccncfext  46629  fourierdlem41  46890  meaiininclem  47228  hoidmvlelem3  47339  hoidmvle  47342  opnvonmbllem1  47374  opnvonmbl  47376  iinhoiicclem  47415  smflim  47519  smflimsuplem7  47568  clnbgrval  48615  clnbgrel  48621  sclnbgrel  48640  isubgredg  48659  isubgruhgr  48661  uhgrimisgrgriclem  48723  uhgrimisgrgric  48724  clnbgrgrimlem  48726  clnbgrgrim  48727  isubgr3stgrlem7  48765  uspgrlimlem1  48781  uspgrlimlem2  48782  uspgrlimlem3  48783  uspgrlim  48785  pgnbgreunbgr  48918  uspgrsprf  48939  iinglb  49628  iscnrm3r  49754  iscnrm3l  49757  imassc  49959  setrecseq  50491  setrec1lem4  50496  setrec2fun  50498