Theorem sseq1d 3966

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseq12d  3968  eqsstrd  3969  ssiun2s  4997  disjxiun  5088  treq  5205  iunopeqop  5461  dfpo2  6243  preddowncl  6279  funimass1  6563  f1imadifssran  6567  feq1  6629  focofo  6748  fvmptss  6941  fvimacnvi  6985  fvimacnvALT  6990  knatar  7291  ovmptss  8023  fnsuppres  8121  frecseq123  8212  csbfrecsg  8214  frrlem1  8216  frrlem3  8218  frrlem4  8219  frrlem13  8228  frrdmcl  8238  fprresex  8240  dfrecs3  8292  oaordi  8461  oaword2  8468  oawordeulem  8469  omword1  8488  oewordri  8507  oeordsuc  8509  nnaordi  8533  nnawordex  8552  naddcllem  8591  naddunif  8608  ereq1  8629  elpm2r  8769  inficl  9309  fipwss  9313  dffi3  9315  hartogslem1  9428  inf3lema  9514  inf3lemd  9517  cantnfle  9561  cantnflem2  9580  ttrclselem1  9615  trcl  9618  tcmin  9631  rankr1ai  9688  rankxplim  9769  scottex  9775  scott0  9776  scottexs  9777  scott0s  9778  karden  9785  cardne  9855  cardaleph  9977  ackbij2  10130  cflim2  10151  cfslb  10154  coftr  10161  fin23lem15  10222  fin23lem32  10232  fin23lem34  10234  fin23lem35  10235  fin23lem36  10236  fin23lem41  10240  isf32lem1  10241  itunitc1  10308  axdc3lem2  10339  ttukeylem1  10397  fpwwe2cbv  10518  fpwwe2lem2  10520  fpwwe2lem4  10522  fpwwe2  10531  fpwwecbv  10532  fpwwelem  10533  canthwelem  10538  canthwe  10539  pwfseqlem4  10550  wunex2  10626  wuncval2  10635  eltsk2g  10639  tskpwss  10640  inar1  10663  grothpw  10714  grothpwex  10715  axgroth6  10716  grothac  10718  peano5uzti  12560  fsuppmapnn0fiub0  13897  relexpnndm  14945  rtrclreclem4  14965  dfrtrcl2  14966  lo1o1  15436  o1lo1  15441  o1lo12  15442  lo1eq  15472  rlimeq  15473  isercoll  15572  prmreclem4  16828  vdwmc  16887  vdwlem1  16890  vdwlem2  16891  vdwlem12  16901  vdwlem13  16902  ramval  16917  ramz2  16933  ramub1lem1  16935  isacs2  17556  isacs1i  17560  mreacs  17561  acsfn  17562  rescabs  17737  ipole  18437  ipodrsima  18444  isacs5  18451  symgsssg  19377  psgnunilem5  19404  sylow1  19513  efgval2  19634  efgsfo  19649  frgpuplem  19682  gsumzf1o  19822  gsumzoppg  19854  dprdcntz  19920  islbs2  21089  frlmssuvc1  21729  frlmssuvc2  21730  frlmsslsp  21731  ismhp  22053  pptbas  22921  pnfnei  23133  mnfnei  23134  iscnp  23150  iscnp4  23176  cnntr  23188  cnconst2  23196  cnpresti  23201  cnprest  23202  isreg  23245  isnrm  23248  isnrm2  23271  perfcls  23278  isreg2  23290  hauscmplem  23319  1stcfb  23358  1stcelcls  23374  1stccnp  23375  txbas  23480  ptbasfi  23494  xkoopn  23502  xkoccn  23532  txcnp  23533  ptcnplem  23534  txdis  23545  txdis1cn  23548  txtube  23553  txkgen  23565  xkohaus  23566  xkoptsub  23567  xkoco1cn  23570  xkoco2cn  23571  xkococnlem  23572  xkococn  23573  xkoinjcn  23600  kqreglem1  23654  kqreglem2  23655  kqnrmlem1  23656  kqnrmlem2  23657  reghmph  23706  nrmhmph  23707  trfil2  23800  ufileu  23832  elfm  23860  elfm2  23861  elfm3  23863  imaelfm  23864  rnelfm  23866  fmfnfmlem2  23868  fmfnfmlem4  23870  fmco  23874  elflim2  23877  flffbas  23908  lmflf  23918  txflf  23919  fclscf  23938  flimfnfcls  23941  cnextcn  23980  symgtgp  24019  ghmcnp  24028  qustgplem  24034  eltsms  24046  ustval  24116  ust0  24133  trust  24142  utoptop  24147  restutop  24150  restutopopn  24151  utopsnneiplem  24160  ucncn  24197  fmucnd  24204  cfilufg  24205  trcfilu  24206  neipcfilu  24208  blssps  24337  blss  24338  ssblex  24341  blin2  24342  metss2  24425  metrest  24437  metcnp3  24453  metustexhalf  24469  metustbl  24479  psmetutop  24480  xrsmopn  24726  recld2  24728  icccmplem1  24736  icccmplem2  24737  icccmp  24739  reconnlem2  24741  lebnumlem3  24887  lebnum  24888  xlebnum  24889  lebnumii  24890  nmhmcn  25045  cfilfval  25189  caubl  25233  caublcls  25234  bcthlem1  25249  bcth  25254  ovolfiniun  25427  ovoliunlem3  25430  ovoliun  25431  ovoliun2  25432  ovoliunnul  25433  voliunlem3  25478  dyadmax  25524  dyadmbllem  25525  dyadmbl  25526  opnmbllem  25527  ellimc2  25803  limcnlp  25804  ellimc3  25805  limcflf  25807  limciun  25820  cpnord  25862  lhop  25946  xrlimcnp  26903  cvxcl  26920  dchrval  27170  noetalem2  27679  madebdayim  27831  madebdaylemold  27841  madebday  27843  bdayle  27859  precsexlem8  28150  ausgrumgri  29143  ausgrusgri  29144  nbgrval  29312  nbgrel  29316  nbumgrvtx  29322  nbgrnself  29335  uvtxel1  29372  wlkonl1iedg  29640  crctcshwlkn0lem6  29791  2wlkdlem10  29911  1wlkdlem4  30115  3wlkdlem6  30140  3wlkdlem10  30144  eupth2lem3lem4  30206  frcond1  30241  frgr1v  30246  nfrgr2v  30247  frgr3vlem1  30248  frgr3vlem2  30249  frgr3v  30250  4cycl2vnunb  30265  n4cyclfrgr  30266  isssp  30699  ubthlem1  30845  shmodi  31365  chsupid  31387  chsscon3  31475  spansncvi  31627  mdslmd1lem3  32302  mdslmd1lem4  32303  mdsymlem5  32382  dmdbr5ati  32397  dmdbr6ati  32398  dmdbr7ati  32399  ssiun2sf  32534  fpwrelmapffslem  32710  prodindf  32839  pwrssmgc  32976  fldgenval  33273  unitprodclb  33349  esplysply  33587  resssra  33594  constrsscn  33748  constrextdg2lem  33756  constrextdg2  33757  txomap  33842  locfinreflem  33848  tpr2rico  33920  pnfneige0  33959  rrhre  34029  dya2icoseg2  34286  omsfval  34302  eulerpartlemt0  34377  eulerpartgbij  34380  eulerpartlemr  34382  eulerpartlemgs2  34388  eulerpartlemn  34389  eulerpart  34390  bnj517  34892  bnj1014  34968  bnj1015  34969  bnj1123  34993  bnj1125  34999  bnj1450  35057  bnj1452  35059  cplgredgex  35153  kur14  35248  cvmliftlem15  35330  cvmlift2lem12  35346  cvmlift2lem13  35347  mclsval  35595  mclsax  35601  mclsppslem  35615  prodeq12sdv  36251  cbvsumdavw2  36328  cbvproddavw2  36329  opnrebl  36353  opnrebl2  36354  ivthALT  36368  neibastop2lem  36393  fnemeet1  36399  filnetlem1  36411  filnetlem4  36414  bj-imdirval3  37217  bj-imdiridlem  37218  rdgssun  37411  lindsadd  37652  lindsenlbs  37654  ptrecube  37659  poimirlem32  37691  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  mblfinlem3  37698  ovoliunnfl  37701  ex-ovoliunnfl  37702  voliunnfl  37703  totbndbnd  37828  heibor1lem  37848  heiborlem10  37859  scottexf  38207  scott0f  38208  relcnveq2  38356  cnvref4  38377  elrelscnveq2  38529  dfcnvrefrels2  38564  dfcnvrefrel2  38566  symrefref2  38599  lcv1  39079  lfl1dim  39159  lfl1dim2N  39160  paddasslem17  39874  dihglblem6  41378  dochvalr  41395  dochord3  41410  lpolconN  41525  lcfls1lem  41572  mapdffval  41664  mapdfval  41665  mapdsn2  41680  mapd0  41703  lspindp5  41808  mapdh8ab  41815  primrootscoprbij  42134  aks6d1c2  42162  aks6d1c6lem3  42204  aks6d1c6lem5  42209  aks6d1c7lem1  42212  ismrcd1  42730  nacsfix  42744  setindtr  43056  hbtlem6  43161  oaabsb  43326  tfsconcatrnss  43382  naddwordnexlem4  43433  clcnvlem  43655  iunrelexpmin1  43740  iunrelexpmin2  43744  relexp0a  43748  cotrcltrcl  43757  trclimalb2  43758  cotrclrcl  43774  sbcheg  43811  clsk1indlem1  44077  isotone1  44080  isotone2  44081  ntrclsiso  44099  ntrclsk2  44100  k0004lem1  44179  k0004lem3  44181  scottelrankd  44279  mnuop123d  44294  mnuprdlem1  44304  mnuprdlem2  44305  mnuunid  44309  mnurndlem1  44313  modelaxreplem1  45010  modelaxreplem2  45011  modelaxrep  45013  ssdec  45124  iinssd  45167  iinssdf  45175  ssnnf1octb  45230  iooiinicc  45581  iooiinioc  45595  icccncfext  45924  fourierdlem41  46185  meaiininclem  46523  hoidmvlelem3  46634  hoidmvle  46637  opnvonmbllem1  46669  opnvonmbl  46671  iinhoiicclem  46710  smflim  46814  smflimsuplem7  46863  clnbgrval  47852  clnbgrel  47858  sclnbgrel  47877  isubgredg  47896  isubgruhgr  47898  uhgrimisgrgriclem  47960  uhgrimisgrgric  47961  clnbgrgrimlem  47963  clnbgrgrim  47964  isubgr3stgrlem7  48002  uspgrlimlem1  48018  uspgrlimlem2  48019  uspgrlimlem3  48020  uspgrlim  48022  pgnbgreunbgr  48155  uspgrsprf  48176  iinglb  48852  iscnrm3r  48978  iscnrm3l  48981  imassc  49184  setrecseq  49716  setrec1lem4  49721  setrec2fun  49723