Theorem sseq1d 3997

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3950

This theorem is referenced by:  sseq12d  3999  eqsstrd  4000  ssiun2s  5030  disjxiun  5122  treq  5249  iunopeqop  5508  dfpo2  6298  preddowncl  6334  funimass1  6629  f1imadifssran  6633  feq1  6697  focofo  6814  fvmptss  7009  fvimacnvi  7053  fvimacnvALT  7058  knatar  7360  ovmptss  8101  fnsuppres  8199  frecseq123  8290  csbfrecsg  8292  frrlem1  8294  frrlem3  8296  frrlem4  8297  frrlem13  8306  frrdmcl  8316  fprresex  8318  wrecseq123OLD  8323  wfrlem1OLD  8331  wfrlem3OLD  8333  wfrdmclOLD  8340  wfrlem15OLD  8346  wfrlem17OLD  8348  dfrecs3  8395  dfrecs3OLD  8396  oaordi  8567  oaword2  8574  oawordeulem  8575  omword1  8594  oewordri  8613  oeordsuc  8615  nnaordi  8639  nnawordex  8658  naddcllem  8697  naddunif  8714  ereq1  8735  elpm2r  8868  inficl  9448  fipwss  9452  dffi3  9454  hartogslem1  9565  inf3lema  9647  inf3lemd  9650  cantnfle  9694  cantnflem2  9713  ttrclselem1  9748  trcl  9751  tcmin  9764  rankr1ai  9821  rankxplim  9902  scottex  9908  scott0  9909  scottexs  9910  scott0s  9911  karden  9918  cardne  9988  cardaleph  10112  ackbij2  10265  cflim2  10286  cfslb  10289  coftr  10296  fin23lem15  10357  fin23lem32  10367  fin23lem34  10369  fin23lem35  10370  fin23lem36  10371  fin23lem41  10375  isf32lem1  10376  itunitc1  10443  axdc3lem2  10474  ttukeylem1  10532  fpwwe2cbv  10653  fpwwe2lem2  10655  fpwwe2lem4  10657  fpwwe2  10666  fpwwecbv  10667  fpwwelem  10668  canthwelem  10673  canthwe  10674  pwfseqlem4  10685  wunex2  10761  wuncval2  10770  eltsk2g  10774  tskpwss  10775  inar1  10798  grothpw  10849  grothpwex  10850  axgroth6  10851  grothac  10853  peano5uzti  12692  fsuppmapnn0fiub0  14017  relexpnndm  15063  rtrclreclem4  15083  dfrtrcl2  15084  lo1o1  15551  o1lo1  15556  o1lo12  15557  lo1eq  15587  rlimeq  15588  isercoll  15687  prmreclem4  16940  vdwmc  16999  vdwlem1  17002  vdwlem2  17003  vdwlem12  17013  vdwlem13  17014  ramval  17029  ramz2  17045  ramub1lem1  17047  isacs2  17672  isacs1i  17676  mreacs  17677  acsfn  17678  rescabs  17853  rescabsOLD  17854  ipole  18553  ipodrsima  18560  isacs5  18567  symgsssg  19458  psgnunilem5  19485  sylow1  19594  efgval2  19715  efgsfo  19730  frgpuplem  19763  gsumzf1o  19903  gsumzoppg  19935  dprdcntz  20001  islbs2  21129  frlmssuvc1  21781  frlmssuvc2  21782  frlmsslsp  21783  ismhp  22111  pptbas  22981  pnfnei  23193  mnfnei  23194  iscnp  23210  iscnp4  23236  cnntr  23248  cnconst2  23256  cnpresti  23261  cnprest  23262  isreg  23305  isnrm  23308  isnrm2  23331  perfcls  23338  isreg2  23350  hauscmplem  23379  1stcfb  23418  1stcelcls  23434  1stccnp  23435  txbas  23540  ptbasfi  23554  xkoopn  23562  xkoccn  23592  txcnp  23593  ptcnplem  23594  txdis  23605  txdis1cn  23608  txtube  23613  txkgen  23625  xkohaus  23626  xkoptsub  23627  xkoco1cn  23630  xkoco2cn  23631  xkococnlem  23632  xkococn  23633  xkoinjcn  23660  kqreglem1  23714  kqreglem2  23715  kqnrmlem1  23716  kqnrmlem2  23717  reghmph  23766  nrmhmph  23767  trfil2  23860  ufileu  23892  elfm  23920  elfm2  23921  elfm3  23923  imaelfm  23924  rnelfm  23926  fmfnfmlem2  23928  fmfnfmlem4  23930  fmco  23934  elflim2  23937  flffbas  23968  lmflf  23978  txflf  23979  fclscf  23998  flimfnfcls  24001  cnextcn  24040  symgtgp  24079  ghmcnp  24088  qustgplem  24094  eltsms  24106  ustval  24176  ust0  24193  trust  24203  utoptop  24208  restutop  24211  restutopopn  24212  utopsnneiplem  24221  ucncn  24258  fmucnd  24265  cfilufg  24266  trcfilu  24267  neipcfilu  24269  blssps  24398  blss  24399  ssblex  24402  blin2  24403  metss2  24488  metrest  24500  metcnp3  24516  metustexhalf  24532  metustbl  24542  psmetutop  24543  xrsmopn  24789  recld2  24791  icccmplem1  24799  icccmplem2  24800  icccmp  24802  reconnlem2  24804  lebnumlem3  24950  lebnum  24951  xlebnum  24952  lebnumii  24953  nmhmcn  25108  cfilfval  25253  caubl  25297  caublcls  25298  bcthlem1  25313  bcth  25318  ovolfiniun  25491  ovoliunlem3  25494  ovoliun  25495  ovoliun2  25496  ovoliunnul  25497  voliunlem3  25542  dyadmax  25588  dyadmbllem  25589  dyadmbl  25590  opnmbllem  25591  ellimc2  25867  limcnlp  25868  ellimc3  25869  limcflf  25871  limciun  25884  cpnord  25926  lhop  26010  xrlimcnp  26966  cvxcl  26983  dchrval  27233  noetalem2  27742  madebdayim  27881  madebdaylemold  27891  madebday  27893  precsexlem8  28193  ausgrumgri  29131  ausgrusgri  29132  nbgrval  29300  nbgrel  29304  nbumgrvtx  29310  nbgrnself  29323  uvtxel1  29360  wlkonl1iedg  29630  crctcshwlkn0lem6  29782  2wlkdlem10  29902  1wlkdlem4  30106  3wlkdlem6  30131  3wlkdlem10  30135  eupth2lem3lem4  30197  frcond1  30232  frgr1v  30237  nfrgr2v  30238  frgr3vlem1  30239  frgr3vlem2  30240  frgr3v  30241  4cycl2vnunb  30256  n4cyclfrgr  30257  isssp  30690  ubthlem1  30836  shmodi  31356  chsupid  31378  chsscon3  31466  spansncvi  31618  mdslmd1lem3  32293  mdslmd1lem4  32294  mdsymlem5  32373  dmdbr5ati  32388  dmdbr6ati  32389  dmdbr7ati  32390  ssiun2sf  32519  fpwrelmapffslem  32690  prodindf  32795  pwrssmgc  32936  fldgenval  33260  unitprodclb  33358  resssra  33579  constrsscn  33722  constrextdg2lem  33730  constrextdg2  33731  txomap  33774  locfinreflem  33780  tpr2rico  33852  pnfneige0  33891  rrhre  33963  dya2icoseg2  34221  omsfval  34237  eulerpartlemt0  34312  eulerpartgbij  34315  eulerpartlemr  34317  eulerpartlemgs2  34323  eulerpartlemn  34324  eulerpart  34325  bnj517  34840  bnj1014  34916  bnj1015  34917  bnj1123  34941  bnj1125  34947  bnj1450  35005  bnj1452  35007  cplgredgex  35067  kur14  35162  cvmliftlem15  35244  cvmlift2lem12  35260  cvmlift2lem13  35261  mclsval  35509  mclsax  35515  mclsppslem  35529  prodeq12sdv  36160  cbvsumdavw2  36237  cbvproddavw2  36238  opnrebl  36262  opnrebl2  36263  ivthALT  36277  neibastop2lem  36302  fnemeet1  36308  filnetlem1  36320  filnetlem4  36323  bj-imdirval3  37126  bj-imdiridlem  37127  rdgssun  37320  lindsadd  37561  lindsenlbs  37563  ptrecube  37568  poimirlem32  37600  opnmbllem0  37604  mblfinlem1  37605  mblfinlem2  37606  mblfinlem3  37607  ovoliunnfl  37610  ex-ovoliunnfl  37611  voliunnfl  37612  totbndbnd  37737  heibor1lem  37757  heiborlem10  37768  scottexf  38116  scott0f  38117  relcnveq2  38265  cnvref4  38292  elrelscnveq2  38435  dfcnvrefrels2  38470  dfcnvrefrel2  38472  symrefref2  38505  lcv1  38983  lfl1dim  39063  lfl1dim2N  39064  paddasslem17  39779  dihglblem6  41283  dochvalr  41300  dochord3  41315  lpolconN  41430  lcfls1lem  41477  mapdffval  41569  mapdfval  41570  mapdsn2  41585  mapd0  41608  lspindp5  41713  mapdh8ab  41720  primrootscoprbij  42044  aks6d1c2  42072  aks6d1c6lem3  42114  aks6d1c6lem5  42119  aks6d1c7lem1  42122  ismrcd1  42654  nacsfix  42668  setindtr  42981  hbtlem6  43086  oaabsb  43252  tfsconcatrnss  43308  naddwordnexlem4  43359  clcnvlem  43581  iunrelexpmin1  43666  iunrelexpmin2  43670  relexp0a  43674  cotrcltrcl  43683  trclimalb2  43684  cotrclrcl  43700  sbcheg  43737  clsk1indlem1  44003  isotone1  44006  isotone2  44007  ntrclsiso  44025  ntrclsk2  44026  k0004lem1  44105  k0004lem3  44107  scottelrankd  44211  mnuop123d  44226  mnuprdlem1  44236  mnuprdlem2  44237  mnuunid  44241  mnurndlem1  44245  modelaxreplem1  44940  modelaxreplem2  44941  modelaxrep  44943  ssdec  45038  iinssd  45081  iinssdf  45089  ssnnf1octb  45144  iooiinicc  45500  iooiinioc  45514  icccncfext  45847  fourierdlem41  46108  meaiininclem  46446  hoidmvlelem3  46557  hoidmvle  46560  opnvonmbllem1  46592  opnvonmbl  46594  iinhoiicclem  46633  smflim  46737  smflimsuplem7  46786  clnbgrval  47755  clnbgrel  47761  sclnbgrel  47779  isubgredg  47798  isubgruhgr  47800  uhgrimisgrgriclem  47844  uhgrimisgrgric  47845  clnbgrgrimlem  47847  clnbgrgrim  47848  isubgr3stgrlem7  47885  uspgrlimlem1  47901  uspgrlimlem2  47902  uspgrlimlem3  47903  uspgrlim  47905  uspgrsprf  48008  iscnrm3r  48793  iscnrm3l  48796  setrecseq  49200  setrec1lem4  49205  setrec2fun  49207