Theorem sseq1d 3970

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseq12d  3972  eqsstrd  3973  ssiun2s  5009  disjxiun  5102  treq  5219  iunopeqop  5495  iunopeqopOLD  5496  dfpo2  6287  preddowncl  6323  funimass1  6607  f1imadifssran  6611  feq1  6673  focofo  6795  fvmptss  6992  fvimacnvi  7037  fvimacnvALT  7042  knatar  7345  ovmptss  8076  fnsuppres  8175  frecseq123  8267  csbfrecsg  8269  frrlem1  8271  frrlem3  8273  frrlem4  8274  frrlem13  8283  frrdmcl  8293  fprresex  8295  dfrecs3  8347  oaordi  8519  oaword2  8526  oawordeulem  8527  omword1  8546  oewordri  8566  oeordsuc  8568  nnaordi  8592  nnawordex  8611  naddcllem  8650  naddunif  8668  ereq1  8690  elpm2r  8830  inficl  9373  fipwss  9377  dffi3  9379  hartogslem1  9492  inf3lema  9581  inf3lemd  9584  cantnfle  9628  cantnflem2  9647  ttrclselem1  9682  trcl  9685  tcmin  9696  rankr1ai  9758  rankxplim  9839  scottex  9847  scott0  9848  scottexs  9849  scott0s  9850  scottelrankd  9861  karden  9869  cardne  9939  cardaleph  10061  ackbij2  10213  cflim2  10235  cfslb  10238  coftr  10245  fin23lem15  10306  fin23lem32  10316  fin23lem34  10318  fin23lem35  10319  fin23lem36  10320  fin23lem41  10324  isf32lem1  10325  itunitc1  10392  axdc3lem2  10423  ttukeylem1  10481  fpwwe2cbv  10603  fpwwe2lem2  10605  fpwwe2lem4  10607  fpwwe2  10616  fpwwecbv  10617  fpwwelem  10618  canthwelem  10623  canthwe  10624  pwfseqlem4  10635  wunex2  10711  wuncval2  10720  eltsk2g  10724  tskpwss  10725  inar1  10748  grothpw  10799  grothpwex  10800  axgroth6  10801  grothac  10803  peano5uzti  12677  fsuppmapnn0fiub0  14020  relexpnndm  15068  rtrclreclem4  15088  dfrtrcl2  15089  lo1o1  15573  o1lo1  15578  o1lo12  15579  lo1eq  15609  rlimeq  15610  isercoll  15709  prmreclem4  16969  vdwmc  17028  vdwlem1  17031  vdwlem2  17032  vdwlem12  17042  vdwlem13  17043  ramval  17058  ramz2  17074  ramub1lem1  17076  isacs2  17699  isacs1i  17703  mreacs  17704  acsfn  17705  rescabs  17880  ipole  18580  ipodrsima  18587  isacs5  18594  symgsssg  19528  psgnunilem5  19555  sylow1  19664  efgval2  19785  efgsfo  19800  frgpuplem  19833  gsumzf1o  19973  gsumzoppg  20005  dprdcntz  20071  islbs2  21247  frlmssuvc1  21904  frlmssuvc2  21905  frlmsslsp  21906  ismhp  22263  pptbas  23126  pnfnei  23338  mnfnei  23339  iscnp  23355  iscnp4  23381  cnntr  23393  cnconst2  23401  cnpresti  23406  cnprest  23407  isreg  23450  isnrm  23453  isnrm2  23476  perfcls  23483  isreg2  23495  hauscmplem  23524  1stcfb  23563  1stcelcls  23579  1stccnp  23580  txbas  23685  ptbasfi  23699  xkoopn  23707  xkoccn  23737  txcnp  23738  ptcnplem  23739  txdis  23750  txdis1cn  23753  txtube  23758  txkgen  23770  xkohaus  23771  xkoptsub  23772  xkoco1cn  23775  xkoco2cn  23776  xkococnlem  23777  xkococn  23778  xkoinjcn  23805  kqreglem1  23859  kqreglem2  23860  kqnrmlem1  23861  kqnrmlem2  23862  reghmph  23911  nrmhmph  23912  trfil2  24005  ufileu  24037  elfm  24065  elfm2  24066  elfm3  24068  imaelfm  24069  rnelfm  24071  fmfnfmlem2  24073  fmfnfmlem4  24075  fmco  24079  elflim2  24082  flffbas  24113  lmflf  24123  txflf  24124  fclscf  24143  flimfnfcls  24146  cnextcn  24185  symgtgp  24224  ghmcnp  24233  qustgplem  24239  eltsms  24251  ustval  24321  ust0  24338  trust  24347  utoptop  24352  restutop  24355  restutopopn  24356  utopsnneiplem  24365  ucncn  24402  fmucnd  24409  cfilufg  24410  trcfilu  24411  neipcfilu  24413  blssps  24542  blss  24543  ssblex  24546  blin2  24547  metss2  24630  metrest  24642  metcnp3  24658  metustexhalf  24674  metustbl  24684  psmetutop  24685  xrsmopn  24931  recld2  24933  icccmplem1  24941  icccmplem2  24942  icccmp  24944  reconnlem2  24946  lebnumlem3  25083  lebnum  25084  xlebnum  25085  lebnumii  25086  nmhmcn  25240  cfilfval  25384  caubl  25428  caublcls  25429  bcthlem1  25444  bcth  25449  ovolfiniun  25621  ovoliunlem3  25624  ovoliun  25625  ovoliun2  25626  ovoliunnul  25627  voliunlem3  25672  dyadmax  25718  dyadmbllem  25719  dyadmbl  25720  opnmbllem  25721  ellimc2  25997  limcnlp  25998  ellimc3  25999  limcflf  26001  limciun  26014  cpnord  26055  lhop  26136  xrlimcnp  27091  cvxcl  27107  dchrval  27356  noetalem2  27864  madebdayim  28039  madebdaylemold  28049  madebday  28051  bdayle  28067  precsexlem8  28365  bdaypw2n0bndlem  28614  bdayfinbndcbv  28617  bdayfinbndlem1  28618  bdayfinbndlem2  28619  bdayfinbnd  28620  lnssplng  29022  ausgrumgri  29426  ausgrusgri  29427  nbgrval  29595  nbgrel  29599  nbumgrvtx  29605  nbgrnself  29618  uvtxel1  29655  wlkonl1iedg  29922  crctcshwlkn0lem6  30073  2wlkdlem10  30193  1wlkdlem4  30400  3wlkdlem6  30425  3wlkdlem10  30429  eupth2lem3lem4  30491  frcond1  30526  frgr1v  30531  nfrgr2v  30532  frgr3vlem1  30533  frgr3vlem2  30534  frgr3v  30535  4cycl2vnunb  30550  n4cyclfrgr  30551  isssp  30985  ubthlem1  31131  shmodi  31651  chsupid  31673  chsscon3  31761  spansncvi  31913  mdslmd1lem3  32588  mdslmd1lem4  32589  mdsymlem5  32668  dmdbr5ati  32683  dmdbr6ati  32684  dmdbr7ati  32685  ssiun2sf  32814  fpwrelmapffslem  32989  prodindf  33095  pwrssmgc  33233  fldgenval  33548  unitprodclb  33618  esplysply  33878  esplyfvaln  33881  esplyind  33882  resssra  33894  constrsscn  34047  constrextdg2lem  34055  constrextdg2  34056  txomap  34141  locfinreflem  34147  tpr2rico  34219  pnfneige0  34258  rrhre  34328  dya2icoseg2  34585  omsfval  34601  eulerpartlemt0  34676  eulerpartgbij  34679  eulerpartlemr  34681  eulerpartlemgs2  34687  eulerpartlemn  34688  eulerpart  34689  bnj517  35190  bnj1014  35266  bnj1015  35267  bnj1123  35291  bnj1125  35297  bnj1450  35355  bnj1452  35357  cplgredgex  35484  kur14  35579  cvmliftlem15  35661  cvmlift2lem12  35677  cvmlift2lem13  35678  mclsval  35926  mclsax  35932  mclsppslem  35946  prodeq12sdv  36591  cbvsumdavw2  36668  cbvproddavw2  36669  opnrebl  36693  opnrebl2  36694  ivthALT  36708  neibastop2lem  36733  fnemeet1  36739  filnetlem1  36751  filnetlem4  36754  ttcmin  36869  dfttc2g  36879  bj-imdirval3  37688  bj-imdiridlem  37689  rdgssun  37884  lindsadd  38124  lindsenlbs  38126  ptrecube  38131  poimirlem32  38163  opnmbllem0  38167  mblfinlem1  38168  mblfinlem2  38169  mblfinlem3  38170  ovoliunnfl  38173  ex-ovoliunnfl  38174  voliunnfl  38175  totbndbnd  38300  heibor1lem  38320  heiborlem10  38331  scottexf  38679  scott0f  38680  relcnveq2  38840  cnvref4  38861  dfcnvrefrels2  39119  dfcnvrefrel2  39121  elrelscnveq2  39140  symrefref2  39158  lcv1  39677  lfl1dim  39757  lfl1dim2N  39758  paddasslem17  40472  dihglblem6  41976  dochvalr  41993  dochord3  42008  lpolconN  42123  lcfls1lem  42170  mapdffval  42262  mapdfval  42263  mapdsn2  42278  mapd0  42301  lspindp5  42406  mapdh8ab  42413  primrootscoprbij  42731  aks6d1c2  42759  aks6d1c6lem3  42801  aks6d1c6lem5  42806  aks6d1c7lem1  42809  ismrcd1  43291  nacsfix  43305  setindtr  43613  hbtlem6  43718  oaabsb  43883  tfsconcatrnss  43939  naddwordnexlem4  43990  clcnvlem  44211  iunrelexpmin1  44296  iunrelexpmin2  44300  relexp0a  44304  cotrcltrcl  44313  trclimalb2  44314  cotrclrcl  44330  sbcheg  44367  clsk1indlem1  44633  isotone1  44636  isotone2  44637  ntrclsiso  44655  ntrclsk2  44656  k0004lem1  44735  k0004lem3  44737  mnuop123d  44836  mnuprdlem1  44846  mnuprdlem2  44847  mnuunid  44851  mnurndlem1  44855  modelaxreplem1  45552  modelaxreplem2  45553  modelaxrep  45555  ssdec  45664  iinssd  45707  iinssdf  45715  ssnnf1octb  45770  iooiinicc  46116  iooiinioc  46130  icccncfext  46459  fourierdlem41  46720  meaiininclem  47058  hoidmvlelem3  47169  hoidmvle  47172  opnvonmbllem1  47204  opnvonmbl  47206  iinhoiicclem  47245  smflim  47349  smflimsuplem7  47398  clnbgrval  48442  clnbgrel  48448  sclnbgrel  48467  isubgredg  48486  isubgruhgr  48488  uhgrimisgrgriclem  48550  uhgrimisgrgric  48551  clnbgrgrimlem  48553  clnbgrgrim  48554  isubgr3stgrlem7  48592  uspgrlimlem1  48608  uspgrlimlem2  48609  uspgrlimlem3  48610  uspgrlim  48612  pgnbgreunbgr  48745  uspgrsprf  48766  iinglb  49451  iscnrm3r  49577  iscnrm3l  49580  imassc  49782  setrecseq  50314  setrec1lem4  50319  setrec2fun  50321