Theorem sseq1d 3969

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3906

This theorem was proved from 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 theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseq12d  3971  eqsstrd  3972  ssiun2s  5014  disjxiun  5107  treq  5226  iunopeqop  5506  iunopeqopOLD  5507  dfpo2  6299  preddowncl  6335  funimass1  6620  feq1  6685  focofo  6807  fvmptss  7004  fvimacnvi  7049  fvimacnvALT  7054  knatar  7357  ovmptss  8089  fnsuppres  8188  frecseq123  8280  csbfrecsg  8282  frrlem1  8284  frrlem3  8286  frrlem4  8287  frrlem13  8296  frrdmcl  8306  fprresex  8308  dfrecs3  8360  oaordi  8532  oaword2  8539  oawordeulem  8540  omword1  8559  oewordri  8579  oeordsuc  8581  nnaordi  8605  nnawordex  8624  naddcllem  8663  naddunif  8681  ereq1  8703  elpm2r  8843  inficl  9386  fipwss  9390  dffi3  9392  hartogslem1  9505  inf3lema  9594  inf3lemd  9597  cantnfle  9641  cantnflem2  9660  ttrclselem1  9695  trcl  9698  tcmin  9709  rankr1ai  9771  rankxplim  9852  scottex  9860  scott0  9861  scottexs  9862  scott0s  9863  scottelrankd  9874  karden  9882  cardne  9952  cardaleph  10074  ackbij2  10226  cflim2  10248  cfslb  10251  coftr  10258  fin23lem15  10319  fin23lem32  10329  fin23lem34  10331  fin23lem35  10332  fin23lem36  10333  fin23lem41  10337  isf32lem1  10338  itunitc1  10405  axdc3lem2  10436  ttukeylem1  10494  fpwwe2cbv  10616  fpwwe2lem2  10618  fpwwe2lem4  10620  fpwwe2  10629  fpwwecbv  10630  fpwwelem  10631  canthwelem  10636  canthwe  10637  pwfseqlem4  10648  wunex2  10724  wuncval2  10733  eltsk2g  10737  tskpwss  10738  inar1  10761  grothpw  10812  grothpwex  10813  axgroth6  10814  grothac  10816  peano5uzti  12687  fsuppmapnn0fiub0  14031  relexpnndm  15080  rtrclreclem4  15100  dfrtrcl2  15101  lo1o1  15585  o1lo1  15590  o1lo12  15591  lo1eq  15621  rlimeq  15622  isercoll  15721  prmreclem4  16980  vdwmc  17039  vdwlem1  17042  vdwlem2  17043  vdwlem12  17053  vdwlem13  17054  ramval  17069  ramz2  17085  ramub1lem1  17087  isacs2  17710  isacs1i  17714  mreacs  17715  acsfn  17716  rescabs  17891  ipole  18591  ipodrsima  18598  isacs5  18605  symgsssg  19538  psgnunilem5  19565  sylow1  19674  efgval2  19795  efgsfo  19810  frgpuplem  19843  gsumzf1o  19983  gsumzoppg  20015  dprdcntz  20081  islbs2  21259  frlmssuvc1  21925  frlmssuvc2  21926  frlmsslsp  21927  ismhp  22284  pptbas  23146  pnfnei  23358  mnfnei  23359  iscnp  23375  iscnp4  23401  cnntr  23413  cnconst2  23421  cnpresti  23426  cnprest  23427  isreg  23470  isnrm  23473  isnrm2  23496  perfcls  23503  isreg2  23515  hauscmplem  23544  1stcfb  23583  1stcelcls  23599  1stccnp  23600  txbas  23705  ptbasfi  23719  xkoopn  23727  xkoccn  23757  txcnp  23758  ptcnplem  23759  txdis  23770  txdis1cn  23773  txtube  23778  txkgen  23790  xkohaus  23791  xkoptsub  23792  xkoco1cn  23795  xkoco2cn  23796  xkococnlem  23797  xkococn  23798  xkoinjcn  23825  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  reghmph  23931  nrmhmph  23932  trfil2  24025  ufileu  24057  elfm  24085  elfm2  24086  elfm3  24088  imaelfm  24089  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  fmco  24099  elflim2  24102  flffbas  24133  lmflf  24143  txflf  24144  fclscf  24163  flimfnfcls  24166  cnextcn  24205  symgtgp  24244  ghmcnp  24253  qustgplem  24259  eltsms  24271  ustval  24341  ust0  24358  trust  24367  utoptop  24372  restutop  24375  restutopopn  24376  utopsnneiplem  24385  ucncn  24422  fmucnd  24429  cfilufg  24430  trcfilu  24431  neipcfilu  24433  blssps  24562  blss  24563  ssblex  24566  blin2  24567  metss2  24650  metrest  24662  metcnp3  24678  metustexhalf  24694  metustbl  24704  psmetutop  24705  xrsmopn  24951  recld2  24953  icccmplem1  24961  icccmplem2  24962  icccmp  24964  reconnlem2  24966  lebnumlem3  25103  lebnum  25104  xlebnum  25105  lebnumii  25106  nmhmcn  25260  cfilfval  25404  caubl  25448  caublcls  25449  bcthlem1  25464  bcth  25469  ovolfiniun  25641  ovoliunlem3  25644  ovoliun  25645  ovoliun2  25646  ovoliunnul  25647  voliunlem3  25692  dyadmax  25738  dyadmbllem  25739  dyadmbl  25740  opnmbllem  25741  ellimc2  26017  limcnlp  26018  ellimc3  26019  limcflf  26021  limciun  26034  cpnord  26075  lhop  26156  xrlimcnp  27111  cvxcl  27127  dchrval  27376  noetalem2  27884  madebdayim  28059  madebdaylemold  28069  madebday  28071  bdayle  28087  precsexlem8  28385  bdaypw2n0bndlem  28634  bdayfinbndcbv  28637  bdayfinbndlem1  28638  bdayfinbndlem2  28639  bdayfinbnd  28640  lnssplng  29052  ausgrumgri  29495  ausgrusgri  29496  nbgrval  29664  nbgrel  29668  nbumgrvtx  29674  nbgrnself  29687  uvtxel1  29724  wlkonl1iedg  29991  crctcshwlkn0lem6  30142  2wlkdlem10  30262  1wlkdlem4  30469  3wlkdlem6  30494  3wlkdlem10  30498  eupth2lem3lem4  30560  frcond1  30595  frgr1v  30600  nfrgr2v  30601  frgr3vlem1  30602  frgr3vlem2  30603  frgr3v  30604  4cycl2vnunb  30619  n4cyclfrgr  30620  isssp  31054  ubthlem1  31200  shmodi  31720  chsupid  31742  chsscon3  31830  spansncvi  31982  mdslmd1lem3  32657  mdslmd1lem4  32658  mdsymlem5  32737  dmdbr5ati  32752  dmdbr6ati  32753  dmdbr7ati  32754  ssiun2sf  32882  fpwrelmapffslem  33055  prodindf  33160  pwrssmgc  33298  fldgenval  33611  unitprodclb  33680  esplysply  33939  esplyfvaln  33942  esplyind  33943  resssra  33955  constrsscn  34108  constrextdg2lem  34116  constrextdg2  34117  txomap  34202  locfinreflem  34208  tpr2rico  34280  pnfneige0  34319  rrhre  34389  dya2icoseg2  34646  omsfval  34662  eulerpartlemt0  34737  eulerpartgbij  34740  eulerpartlemr  34742  eulerpartlemgs2  34748  eulerpartlemn  34749  eulerpart  34750  bnj517  35251  bnj1014  35327  bnj1015  35328  bnj1123  35352  bnj1125  35358  bnj1450  35416  bnj1452  35418  elscott  35488  elkarden  35546  cplgredgex  35591  kur14  35686  cvmliftlem15  35768  cvmlift2lem12  35784  cvmlift2lem13  35785  mclsval  36033  mclsax  36039  mclsppslem  36053  prodeq12sdv  36708  cbvsumdavw2  36785  cbvproddavw2  36786  opnrebl  36809  opnrebl2  36810  ivthALT  36824  neibastop2lem  36849  fnemeet1  36855  filnetlem1  36867  filnetlem4  36870  ttcmin  36985  dfttc2g  36995  bj-imdirval3  37806  bj-imdiridlem  37807  rdgssun  38002  lindsadd  38242  lindsenlbs  38244  ptrecube  38249  poimirlem32  38281  opnmbllem0  38285  mblfinlem1  38286  mblfinlem2  38287  mblfinlem3  38288  ovoliunnfl  38291  ex-ovoliunnfl  38292  voliunnfl  38293  totbndbnd  38418  heibor1lem  38438  heiborlem10  38449  scottexf  38795  scott0f  38796  relcnveq2  38956  cnvref4  38977  dfcnvrefrels2  39235  dfcnvrefrel2  39237  elrelscnveq2  39256  symrefref2  39274  lcv1  39793  lfl1dim  39873  lfl1dim2N  39874  paddasslem17  40588  dihglblem6  42092  dochvalr  42109  dochord3  42124  lpolconN  42239  lcfls1lem  42286  mapdffval  42378  mapdfval  42379  mapdsn2  42394  mapd0  42417  lspindp5  42522  mapdh8ab  42529  primrootscoprbij  42847  aks6d1c2  42875  aks6d1c6lem3  42917  aks6d1c6lem5  42922  aks6d1c7lem1  42925  ismrcd1  43409  nacsfix  43423  setindtr  43731  hbtlem6  43836  oaabsb  44001  tfsconcatrnss  44057  naddwordnexlem4  44108  clcnvlem  44329  iunrelexpmin1  44414  iunrelexpmin2  44418  relexp0a  44422  cotrcltrcl  44431  trclimalb2  44432  cotrclrcl  44448  sbcheg  44485  clsk1indlem1  44751  isotone1  44754  isotone2  44755  ntrclsiso  44773  ntrclsk2  44774  k0004lem1  44853  k0004lem3  44855  mnuop123d  44952  mnuprdlem1  44962  mnuprdlem2  44963  mnuunid  44967  mnurndlem1  44971  modelaxreplem1  45667  modelaxreplem2  45668  modelaxrep  45670  ssdec  45786  iinssd  45829  iinssdf  45837  ssnnf1octb  45892  iooiinicc  46238  iooiinioc  46252  icccncfext  46581  fourierdlem41  46842  meaiininclem  47180  hoidmvlelem3  47291  hoidmvle  47294  opnvonmbllem1  47326  opnvonmbl  47328  iinhoiicclem  47367  smflim  47471  smflimsuplem7  47520  clnbgrval  48564  clnbgrel  48570  sclnbgrel  48589  isubgredg  48608  isubgruhgr  48610  uhgrimisgrgriclem  48672  uhgrimisgrgric  48673  clnbgrgrimlem  48675  clnbgrgrim  48676  isubgr3stgrlem7  48714  uspgrlimlem1  48730  uspgrlimlem2  48731  uspgrlimlem3  48732  uspgrlim  48734  pgnbgreunbgr  48867  uspgrsprf  48888  iinglb  49577  iscnrm3r  49703  iscnrm3l  49706  imassc  49908  setrecseq  50440  setrec1lem4  50445  setrec2fun  50447