Theorem sseq1d 3967

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  sseq12d  3969  eqsstrd  3970  ssiun2s  5006  disjxiun  5097  treq  5214  iunopeqop  5477  dfpo2  6262  preddowncl  6298  funimass1  6582  f1imadifssran  6586  feq1  6648  focofo  6767  fvmptss  6962  fvimacnvi  7006  fvimacnvALT  7011  knatar  7313  ovmptss  8045  fnsuppres  8143  frecseq123  8234  csbfrecsg  8236  frrlem1  8238  frrlem3  8240  frrlem4  8241  frrlem13  8250  frrdmcl  8260  fprresex  8262  dfrecs3  8314  oaordi  8483  oaword2  8490  oawordeulem  8491  omword1  8510  oewordri  8530  oeordsuc  8532  nnaordi  8556  nnawordex  8575  naddcllem  8614  naddunif  8631  ereq1  8653  elpm2r  8794  inficl  9340  fipwss  9344  dffi3  9346  hartogslem1  9459  inf3lema  9545  inf3lemd  9548  cantnfle  9592  cantnflem2  9611  ttrclselem1  9646  trcl  9649  tcmin  9660  rankr1ai  9722  rankxplim  9803  scottex  9809  scott0  9810  scottexs  9811  scott0s  9812  karden  9819  cardne  9889  cardaleph  10011  ackbij2  10164  cflim2  10185  cfslb  10188  coftr  10195  fin23lem15  10256  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem36  10270  fin23lem41  10274  isf32lem1  10275  itunitc1  10342  axdc3lem2  10373  ttukeylem1  10431  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwe2  10566  fpwwecbv  10567  fpwwelem  10568  canthwelem  10573  canthwe  10574  pwfseqlem4  10585  wunex2  10661  wuncval2  10670  eltsk2g  10674  tskpwss  10675  inar1  10698  grothpw  10749  grothpwex  10750  axgroth6  10751  grothac  10753  peano5uzti  12594  fsuppmapnn0fiub0  13928  relexpnndm  14976  rtrclreclem4  14996  dfrtrcl2  14997  lo1o1  15467  o1lo1  15472  o1lo12  15473  lo1eq  15503  rlimeq  15504  isercoll  15603  prmreclem4  16859  vdwmc  16918  vdwlem1  16921  vdwlem2  16922  vdwlem12  16932  vdwlem13  16933  ramval  16948  ramz2  16964  ramub1lem1  16966  isacs2  17588  isacs1i  17592  mreacs  17593  acsfn  17594  rescabs  17769  ipole  18469  ipodrsima  18476  isacs5  18483  symgsssg  19408  psgnunilem5  19435  sylow1  19544  efgval2  19665  efgsfo  19680  frgpuplem  19713  gsumzf1o  19853  gsumzoppg  19885  dprdcntz  19951  islbs2  21121  frlmssuvc1  21761  frlmssuvc2  21762  frlmsslsp  21763  ismhp  22095  pptbas  22964  pnfnei  23176  mnfnei  23177  iscnp  23193  iscnp4  23219  cnntr  23231  cnconst2  23239  cnpresti  23244  cnprest  23245  isreg  23288  isnrm  23291  isnrm2  23314  perfcls  23321  isreg2  23333  hauscmplem  23362  1stcfb  23401  1stcelcls  23417  1stccnp  23418  txbas  23523  ptbasfi  23537  xkoopn  23545  xkoccn  23575  txcnp  23576  ptcnplem  23577  txdis  23588  txdis1cn  23591  txtube  23596  txkgen  23608  xkohaus  23609  xkoptsub  23610  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  xkococn  23616  xkoinjcn  23643  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  reghmph  23749  nrmhmph  23750  trfil2  23843  ufileu  23875  elfm  23903  elfm2  23904  elfm3  23906  imaelfm  23907  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fmco  23917  elflim2  23920  flffbas  23951  lmflf  23961  txflf  23962  fclscf  23981  flimfnfcls  23984  cnextcn  24023  symgtgp  24062  ghmcnp  24071  qustgplem  24077  eltsms  24089  ustval  24159  ust0  24176  trust  24185  utoptop  24190  restutop  24193  restutopopn  24194  utopsnneiplem  24203  ucncn  24240  fmucnd  24247  cfilufg  24248  trcfilu  24249  neipcfilu  24251  blssps  24380  blss  24381  ssblex  24384  blin2  24385  metss2  24468  metrest  24480  metcnp3  24496  metustexhalf  24512  metustbl  24522  psmetutop  24523  xrsmopn  24769  recld2  24771  icccmplem1  24779  icccmplem2  24780  icccmp  24782  reconnlem2  24784  lebnumlem3  24930  lebnum  24931  xlebnum  24932  lebnumii  24933  nmhmcn  25088  cfilfval  25232  caubl  25276  caublcls  25277  bcthlem1  25292  bcth  25297  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  ovoliunnul  25476  voliunlem3  25521  dyadmax  25567  dyadmbllem  25568  dyadmbl  25569  opnmbllem  25570  ellimc2  25846  limcnlp  25847  ellimc3  25848  limcflf  25850  limciun  25863  cpnord  25905  lhop  25989  xrlimcnp  26946  cvxcl  26963  dchrval  27213  noetalem2  27722  madebdayim  27896  madebdaylemold  27906  madebday  27908  bdayle  27924  precsexlem8  28222  bdaypw2n0bndlem  28471  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  bdayfinbnd  28477  ausgrumgri  29252  ausgrusgri  29253  nbgrval  29421  nbgrel  29425  nbumgrvtx  29431  nbgrnself  29444  uvtxel1  29481  wlkonl1iedg  29749  crctcshwlkn0lem6  29900  2wlkdlem10  30020  1wlkdlem4  30227  3wlkdlem6  30252  3wlkdlem10  30256  eupth2lem3lem4  30318  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3vlem1  30360  frgr3vlem2  30361  frgr3v  30362  4cycl2vnunb  30377  n4cyclfrgr  30378  isssp  30811  ubthlem1  30957  shmodi  31477  chsupid  31499  chsscon3  31587  spansncvi  31739  mdslmd1lem3  32414  mdslmd1lem4  32415  mdsymlem5  32494  dmdbr5ati  32509  dmdbr6ati  32510  dmdbr7ati  32511  ssiun2sf  32645  fpwrelmapffslem  32821  prodindf  32954  pwrssmgc  33092  fldgenval  33405  unitprodclb  33481  esplysply  33747  esplyfvaln  33750  esplyind  33751  resssra  33763  constrsscn  33917  constrextdg2lem  33925  constrextdg2  33926  txomap  34011  locfinreflem  34017  tpr2rico  34089  pnfneige0  34128  rrhre  34198  dya2icoseg2  34455  omsfval  34471  eulerpartlemt0  34546  eulerpartgbij  34549  eulerpartlemr  34551  eulerpartlemgs2  34557  eulerpartlemn  34558  eulerpart  34559  bnj517  35060  bnj1014  35136  bnj1015  35137  bnj1123  35161  bnj1125  35167  bnj1450  35225  bnj1452  35227  cplgredgex  35334  kur14  35429  cvmliftlem15  35511  cvmlift2lem12  35527  cvmlift2lem13  35528  mclsval  35776  mclsax  35782  mclsppslem  35796  prodeq12sdv  36431  cbvsumdavw2  36508  cbvproddavw2  36509  opnrebl  36533  opnrebl2  36534  ivthALT  36548  neibastop2lem  36573  fnemeet1  36579  filnetlem1  36591  filnetlem4  36594  bj-imdirval3  37433  bj-imdiridlem  37434  rdgssun  37627  lindsadd  37858  lindsenlbs  37860  ptrecube  37865  poimirlem32  37897  opnmbllem0  37901  mblfinlem1  37902  mblfinlem2  37903  mblfinlem3  37904  ovoliunnfl  37907  ex-ovoliunnfl  37908  voliunnfl  37909  totbndbnd  38034  heibor1lem  38054  heiborlem10  38065  scottexf  38413  scott0f  38414  relcnveq2  38574  cnvref4  38595  dfcnvrefrels2  38853  dfcnvrefrel2  38855  elrelscnveq2  38874  symrefref2  38892  lcv1  39411  lfl1dim  39491  lfl1dim2N  39492  paddasslem17  40206  dihglblem6  41710  dochvalr  41727  dochord3  41742  lpolconN  41857  lcfls1lem  41904  mapdffval  41996  mapdfval  41997  mapdsn2  42012  mapd0  42035  lspindp5  42140  mapdh8ab  42147  primrootscoprbij  42466  aks6d1c2  42494  aks6d1c6lem3  42536  aks6d1c6lem5  42541  aks6d1c7lem1  42544  ismrcd1  43049  nacsfix  43063  setindtr  43375  hbtlem6  43480  oaabsb  43645  tfsconcatrnss  43701  naddwordnexlem4  43752  clcnvlem  43973  iunrelexpmin1  44058  iunrelexpmin2  44062  relexp0a  44066  cotrcltrcl  44075  trclimalb2  44076  cotrclrcl  44092  sbcheg  44129  clsk1indlem1  44395  isotone1  44398  isotone2  44399  ntrclsiso  44417  ntrclsk2  44418  k0004lem1  44497  k0004lem3  44499  scottelrankd  44597  mnuop123d  44612  mnuprdlem1  44622  mnuprdlem2  44623  mnuunid  44627  mnurndlem1  44631  modelaxreplem1  45328  modelaxreplem2  45329  modelaxrep  45331  ssdec  45441  iinssd  45484  iinssdf  45492  ssnnf1octb  45547  iooiinicc  45896  iooiinioc  45910  icccncfext  46239  fourierdlem41  46500  meaiininclem  46838  hoidmvlelem3  46949  hoidmvle  46952  opnvonmbllem1  46984  opnvonmbl  46986  iinhoiicclem  47025  smflim  47129  smflimsuplem7  47178  clnbgrval  48176  clnbgrel  48182  sclnbgrel  48201  isubgredg  48220  isubgruhgr  48222  uhgrimisgrgriclem  48284  uhgrimisgrgric  48285  clnbgrgrimlem  48287  clnbgrgrim  48288  isubgr3stgrlem7  48326  uspgrlimlem1  48342  uspgrlimlem2  48343  uspgrlimlem3  48344  uspgrlim  48346  pgnbgreunbgr  48479  uspgrsprf  48500  iinglb  49175  iscnrm3r  49301  iscnrm3l  49304  imassc  49506  setrecseq  50038  setrec1lem4  50043  setrec2fun  50045