Theorem sseq1d 3965

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  sseq12d  3967  eqsstrd  3968  ssiun2s  5004  disjxiun  5095  treq  5212  iunopeqop  5469  dfpo2  6254  preddowncl  6290  funimass1  6574  f1imadifssran  6578  feq1  6640  focofo  6759  fvmptss  6953  fvimacnvi  6997  fvimacnvALT  7002  knatar  7303  ovmptss  8035  fnsuppres  8133  frecseq123  8224  csbfrecsg  8226  frrlem1  8228  frrlem3  8230  frrlem4  8231  frrlem13  8240  frrdmcl  8250  fprresex  8252  dfrecs3  8304  oaordi  8473  oaword2  8480  oawordeulem  8481  omword1  8500  oewordri  8520  oeordsuc  8522  nnaordi  8546  nnawordex  8565  naddcllem  8604  naddunif  8621  ereq1  8642  elpm2r  8782  inficl  9328  fipwss  9332  dffi3  9334  hartogslem1  9447  inf3lema  9533  inf3lemd  9536  cantnfle  9580  cantnflem2  9599  ttrclselem1  9634  trcl  9637  tcmin  9648  rankr1ai  9710  rankxplim  9791  scottex  9797  scott0  9798  scottexs  9799  scott0s  9800  karden  9807  cardne  9877  cardaleph  9999  ackbij2  10152  cflim2  10173  cfslb  10176  coftr  10183  fin23lem15  10244  fin23lem32  10254  fin23lem34  10256  fin23lem35  10257  fin23lem36  10258  fin23lem41  10262  isf32lem1  10263  itunitc1  10330  axdc3lem2  10361  ttukeylem1  10419  fpwwe2cbv  10541  fpwwe2lem2  10543  fpwwe2lem4  10545  fpwwe2  10554  fpwwecbv  10555  fpwwelem  10556  canthwelem  10561  canthwe  10562  pwfseqlem4  10573  wunex2  10649  wuncval2  10658  eltsk2g  10662  tskpwss  10663  inar1  10686  grothpw  10737  grothpwex  10738  axgroth6  10739  grothac  10741  peano5uzti  12582  fsuppmapnn0fiub0  13916  relexpnndm  14964  rtrclreclem4  14984  dfrtrcl2  14985  lo1o1  15455  o1lo1  15460  o1lo12  15461  lo1eq  15491  rlimeq  15492  isercoll  15591  prmreclem4  16847  vdwmc  16906  vdwlem1  16909  vdwlem2  16910  vdwlem12  16920  vdwlem13  16921  ramval  16936  ramz2  16952  ramub1lem1  16954  isacs2  17576  isacs1i  17580  mreacs  17581  acsfn  17582  rescabs  17757  ipole  18457  ipodrsima  18464  isacs5  18471  symgsssg  19396  psgnunilem5  19423  sylow1  19532  efgval2  19653  efgsfo  19668  frgpuplem  19701  gsumzf1o  19841  gsumzoppg  19873  dprdcntz  19939  islbs2  21109  frlmssuvc1  21749  frlmssuvc2  21750  frlmsslsp  21751  ismhp  22083  pptbas  22952  pnfnei  23164  mnfnei  23165  iscnp  23181  iscnp4  23207  cnntr  23219  cnconst2  23227  cnpresti  23232  cnprest  23233  isreg  23276  isnrm  23279  isnrm2  23302  perfcls  23309  isreg2  23321  hauscmplem  23350  1stcfb  23389  1stcelcls  23405  1stccnp  23406  txbas  23511  ptbasfi  23525  xkoopn  23533  xkoccn  23563  txcnp  23564  ptcnplem  23565  txdis  23576  txdis1cn  23579  txtube  23584  txkgen  23596  xkohaus  23597  xkoptsub  23598  xkoco1cn  23601  xkoco2cn  23602  xkococnlem  23603  xkococn  23604  xkoinjcn  23631  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  reghmph  23737  nrmhmph  23738  trfil2  23831  ufileu  23863  elfm  23891  elfm2  23892  elfm3  23894  imaelfm  23895  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fmco  23905  elflim2  23908  flffbas  23939  lmflf  23949  txflf  23950  fclscf  23969  flimfnfcls  23972  cnextcn  24011  symgtgp  24050  ghmcnp  24059  qustgplem  24065  eltsms  24077  ustval  24147  ust0  24164  trust  24173  utoptop  24178  restutop  24181  restutopopn  24182  utopsnneiplem  24191  ucncn  24228  fmucnd  24235  cfilufg  24236  trcfilu  24237  neipcfilu  24239  blssps  24368  blss  24369  ssblex  24372  blin2  24373  metss2  24456  metrest  24468  metcnp3  24484  metustexhalf  24500  metustbl  24510  psmetutop  24511  xrsmopn  24757  recld2  24759  icccmplem1  24767  icccmplem2  24768  icccmp  24770  reconnlem2  24772  lebnumlem3  24918  lebnum  24919  xlebnum  24920  lebnumii  24921  nmhmcn  25076  cfilfval  25220  caubl  25264  caublcls  25265  bcthlem1  25280  bcth  25285  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  ovoliunnul  25464  voliunlem3  25509  dyadmax  25555  dyadmbllem  25556  dyadmbl  25557  opnmbllem  25558  ellimc2  25834  limcnlp  25835  ellimc3  25836  limcflf  25838  limciun  25851  cpnord  25893  lhop  25977  xrlimcnp  26934  cvxcl  26951  dchrval  27201  noetalem2  27710  madebdayim  27884  madebdaylemold  27894  madebday  27896  bdayle  27912  precsexlem8  28210  bdaypw2n0bndlem  28459  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  bdayfinbnd  28465  ausgrumgri  29240  ausgrusgri  29241  nbgrval  29409  nbgrel  29413  nbumgrvtx  29419  nbgrnself  29432  uvtxel1  29469  wlkonl1iedg  29737  crctcshwlkn0lem6  29888  2wlkdlem10  30008  1wlkdlem4  30215  3wlkdlem6  30240  3wlkdlem10  30244  eupth2lem3lem4  30306  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3vlem1  30348  frgr3vlem2  30349  frgr3v  30350  4cycl2vnunb  30365  n4cyclfrgr  30366  isssp  30799  ubthlem1  30945  shmodi  31465  chsupid  31487  chsscon3  31575  spansncvi  31727  mdslmd1lem3  32402  mdslmd1lem4  32403  mdsymlem5  32482  dmdbr5ati  32497  dmdbr6ati  32498  dmdbr7ati  32499  ssiun2sf  32634  fpwrelmapffslem  32811  prodindf  32944  pwrssmgc  33082  fldgenval  33394  unitprodclb  33470  esplysply  33729  esplyind  33731  resssra  33743  constrsscn  33897  constrextdg2lem  33905  constrextdg2  33906  txomap  33991  locfinreflem  33997  tpr2rico  34069  pnfneige0  34108  rrhre  34178  dya2icoseg2  34435  omsfval  34451  eulerpartlemt0  34526  eulerpartgbij  34529  eulerpartlemr  34531  eulerpartlemgs2  34537  eulerpartlemn  34538  eulerpart  34539  bnj517  35041  bnj1014  35117  bnj1015  35118  bnj1123  35142  bnj1125  35148  bnj1450  35206  bnj1452  35208  cplgredgex  35315  kur14  35410  cvmliftlem15  35492  cvmlift2lem12  35508  cvmlift2lem13  35509  mclsval  35757  mclsax  35763  mclsppslem  35777  prodeq12sdv  36412  cbvsumdavw2  36489  cbvproddavw2  36490  opnrebl  36514  opnrebl2  36515  ivthALT  36529  neibastop2lem  36554  fnemeet1  36560  filnetlem1  36572  filnetlem4  36575  bj-imdirval3  37385  bj-imdiridlem  37386  rdgssun  37579  lindsadd  37810  lindsenlbs  37812  ptrecube  37817  poimirlem32  37849  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  mblfinlem3  37856  ovoliunnfl  37859  ex-ovoliunnfl  37860  voliunnfl  37861  totbndbnd  37986  heibor1lem  38006  heiborlem10  38017  scottexf  38365  scott0f  38366  relcnveq2  38518  cnvref4  38539  dfcnvrefrels2  38777  dfcnvrefrel2  38779  elrelscnveq2  38798  symrefref2  38816  lcv1  39297  lfl1dim  39377  lfl1dim2N  39378  paddasslem17  40092  dihglblem6  41596  dochvalr  41613  dochord3  41628  lpolconN  41743  lcfls1lem  41790  mapdffval  41882  mapdfval  41883  mapdsn2  41898  mapd0  41921  lspindp5  42026  mapdh8ab  42033  primrootscoprbij  42352  aks6d1c2  42380  aks6d1c6lem3  42422  aks6d1c6lem5  42427  aks6d1c7lem1  42430  ismrcd1  42936  nacsfix  42950  setindtr  43262  hbtlem6  43367  oaabsb  43532  tfsconcatrnss  43588  naddwordnexlem4  43639  clcnvlem  43860  iunrelexpmin1  43945  iunrelexpmin2  43949  relexp0a  43953  cotrcltrcl  43962  trclimalb2  43963  cotrclrcl  43979  sbcheg  44016  clsk1indlem1  44282  isotone1  44285  isotone2  44286  ntrclsiso  44304  ntrclsk2  44305  k0004lem1  44384  k0004lem3  44386  scottelrankd  44484  mnuop123d  44499  mnuprdlem1  44509  mnuprdlem2  44510  mnuunid  44514  mnurndlem1  44518  modelaxreplem1  45215  modelaxreplem2  45216  modelaxrep  45218  ssdec  45328  iinssd  45371  iinssdf  45379  ssnnf1octb  45434  iooiinicc  45784  iooiinioc  45798  icccncfext  46127  fourierdlem41  46388  meaiininclem  46726  hoidmvlelem3  46837  hoidmvle  46840  opnvonmbllem1  46872  opnvonmbl  46874  iinhoiicclem  46913  smflim  47017  smflimsuplem7  47066  clnbgrval  48064  clnbgrel  48070  sclnbgrel  48089  isubgredg  48108  isubgruhgr  48110  uhgrimisgrgriclem  48172  uhgrimisgrgric  48173  clnbgrgrimlem  48175  clnbgrgrim  48176  isubgr3stgrlem7  48214  uspgrlimlem1  48230  uspgrlimlem2  48231  uspgrlimlem3  48232  uspgrlim  48234  pgnbgreunbgr  48367  uspgrsprf  48388  iinglb  49063  iscnrm3r  49189  iscnrm3l  49192  imassc  49394  setrecseq  49926  setrec1lem4  49931  setrec2fun  49933