Theorem sseq1d 3978

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  sseq12d  3980  eqsstrd  3985  ssiun2s  5013  disjxiun  5107  treq  5235  iunopeqop  5483  dfpo2  6253  preddowncl  6291  funimass1  6588  feq1  6654  focofo  6774  fvmptss  6965  fvimacnvi  7007  fvimacnvALT  7012  knatar  7307  ovmptss  8030  fnsuppres  8127  frecseq123  8218  csbfrecsg  8220  frrlem1  8222  frrlem3  8224  frrlem4  8225  frrlem13  8234  frrdmcl  8244  fprresex  8246  wrecseq123OLD  8251  wfrlem1OLD  8259  wfrlem3OLD  8261  wfrdmclOLD  8268  wfrlem15OLD  8274  wfrlem17OLD  8276  dfrecs3  8323  dfrecs3OLD  8324  oaordi  8498  oaword2  8505  oawordeulem  8506  omword1  8525  oewordri  8544  oeordsuc  8546  nnaordi  8570  nnawordex  8589  naddcllem  8627  naddunif  8644  ereq1  8662  elpm2r  8790  inficl  9370  fipwss  9374  dffi3  9376  hartogslem1  9487  inf3lema  9569  inf3lemd  9572  cantnfle  9616  cantnflem2  9635  ttrclselem1  9670  trcl  9673  tcmin  9686  rankr1ai  9743  rankxplim  9824  scottex  9830  scott0  9831  scottexs  9832  scott0s  9833  karden  9840  cardne  9910  cardaleph  10034  ackbij2  10188  cflim2  10208  cfslb  10211  coftr  10218  fin23lem15  10279  fin23lem32  10289  fin23lem34  10291  fin23lem35  10292  fin23lem36  10293  fin23lem41  10297  isf32lem1  10298  itunitc1  10365  axdc3lem2  10396  ttukeylem1  10454  fpwwe2cbv  10575  fpwwe2lem2  10577  fpwwe2  10588  fpwwecbv  10589  fpwwelem  10590  canthwelem  10595  canthwe  10596  wunex2  10683  wuncval2  10692  eltsk2g  10696  tskpwss  10697  inar1  10720  grothpw  10771  grothpwex  10772  axgroth6  10773  grothac  10775  peano5uzti  12602  fsuppmapnn0fiub0  13908  relexpnndm  14938  rtrclreclem4  14958  dfrtrcl2  14959  lo1o1  15426  o1lo1  15431  o1lo12  15432  lo1eq  15462  rlimeq  15463  isercoll  15564  prmreclem4  16802  vdwmc  16861  vdwlem1  16864  vdwlem2  16865  vdwlem12  16875  vdwlem13  16876  ramval  16891  ramz2  16907  ramub1lem1  16909  isacs2  17547  isacs1i  17551  mreacs  17552  acsfn  17553  rescabs  17732  rescabsOLD  17733  ipole  18437  ipodrsima  18444  isacs5  18451  symgsssg  19263  psgnunilem5  19290  sylow1  19399  efgval2  19520  efgsfo  19535  frgpuplem  19568  gsumzf1o  19703  gsumzoppg  19735  dprdcntz  19801  islbs2  20674  frlmssuvc1  21237  frlmssuvc2  21238  frlmsslsp  21239  ismhp  21568  pptbas  22395  pnfnei  22608  mnfnei  22609  iscnp  22625  iscnp4  22651  cnntr  22663  cnconst2  22671  cnpresti  22676  cnprest  22677  isreg  22720  isnrm  22723  isnrm2  22746  perfcls  22753  isreg2  22765  hauscmplem  22794  1stcfb  22833  1stcelcls  22849  1stccnp  22850  txbas  22955  ptbasfi  22969  xkoopn  22977  xkoccn  23007  txcnp  23008  ptcnplem  23009  txdis  23020  txdis1cn  23023  txtube  23028  txkgen  23040  xkohaus  23041  xkoptsub  23042  xkoco1cn  23045  xkoco2cn  23046  xkococnlem  23047  xkococn  23048  xkoinjcn  23075  kqreglem1  23129  kqreglem2  23130  kqnrmlem1  23131  kqnrmlem2  23132  reghmph  23181  nrmhmph  23182  trfil2  23275  ufileu  23307  elfm  23335  elfm2  23336  elfm3  23338  imaelfm  23339  rnelfm  23341  fmfnfmlem2  23343  fmfnfmlem4  23345  fmco  23349  elflim2  23352  flffbas  23383  lmflf  23393  txflf  23394  fclscf  23413  flimfnfcls  23416  cnextcn  23455  symgtgp  23494  ghmcnp  23503  qustgplem  23509  eltsms  23521  ustval  23591  ust0  23608  trust  23618  utoptop  23623  restutop  23626  restutopopn  23627  utopsnneiplem  23636  ucncn  23674  fmucnd  23681  cfilufg  23682  trcfilu  23683  neipcfilu  23685  blssps  23814  blss  23815  ssblex  23818  blin2  23819  metss2  23905  metrest  23917  metcnp3  23933  metustexhalf  23949  metustbl  23959  psmetutop  23960  xrsmopn  24212  recld2  24214  icccmplem1  24222  icccmplem2  24223  icccmp  24225  reconnlem2  24227  lebnumlem3  24363  lebnum  24364  xlebnum  24365  lebnumii  24366  nmhmcn  24520  cfilfval  24665  caubl  24709  caublcls  24710  bcthlem1  24725  bcth  24730  ovolfiniun  24902  ovoliunlem3  24905  ovoliun  24906  ovoliun2  24907  ovoliunnul  24908  voliunlem3  24953  dyadmax  24999  dyadmbllem  25000  dyadmbl  25001  opnmbllem  25002  ellimc2  25278  limcnlp  25279  ellimc3  25280  limcflf  25282  limciun  25295  cpnord  25336  lhop  25417  xrlimcnp  26355  cvxcl  26371  dchrval  26619  noetalem2  27127  madebdayim  27260  madebdaylemold  27270  madebday  27272  mulsproplem1  27422  ausgrumgri  28181  ausgrusgri  28182  nbgrval  28347  nbgrel  28351  nbumgrvtx  28357  nbgrnself  28370  uvtxel1  28407  wlkonl1iedg  28676  crctcshwlkn0lem6  28823  2wlkdlem10  28943  1wlkdlem4  29147  3wlkdlem6  29172  3wlkdlem10  29176  eupth2lem3lem4  29238  frcond1  29273  frgr1v  29278  nfrgr2v  29279  frgr3vlem1  29280  frgr3vlem2  29281  frgr3v  29282  4cycl2vnunb  29297  n4cyclfrgr  29298  isssp  29729  ubthlem1  29875  shmodi  30395  chsupid  30417  chsscon3  30505  spansncvi  30657  mdslmd1lem3  31332  mdslmd1lem4  31333  mdsymlem5  31412  dmdbr5ati  31427  dmdbr6ati  31428  dmdbr7ati  31429  ssiun2sf  31545  fpwrelmapffslem  31717  pwrssmgc  31930  fldgenval  32150  txomap  32504  locfinreflem  32510  tpr2rico  32582  pnfneige0  32621  rrhre  32691  prodindf  32711  dya2icoseg2  32967  omsfval  32983  eulerpartlemt0  33058  eulerpartgbij  33061  eulerpartlemr  33063  eulerpartlemgs2  33069  eulerpartlemn  33070  eulerpart  33071  bnj517  33586  bnj1014  33662  bnj1015  33663  bnj1123  33687  bnj1125  33693  bnj1450  33751  bnj1452  33753  cplgredgex  33801  kur14  33897  cvmliftlem15  33979  cvmlift2lem12  33995  cvmlift2lem13  33996  mclsval  34244  mclsax  34250  mclsppslem  34264  opnrebl  34868  opnrebl2  34869  ivthALT  34883  neibastop2lem  34908  fnemeet1  34914  filnetlem1  34926  filnetlem4  34929  bj-imdirval3  35728  bj-imdiridlem  35729  rdgssun  35922  lindsadd  36144  lindsenlbs  36146  ptrecube  36151  poimirlem32  36183  opnmbllem0  36187  mblfinlem1  36188  mblfinlem2  36189  mblfinlem3  36190  ovoliunnfl  36193  ex-ovoliunnfl  36194  voliunnfl  36195  totbndbnd  36321  heibor1lem  36341  heiborlem10  36352  scottexf  36700  scott0f  36701  relcnveq2  36857  cnvref4  36884  elrelscnveq2  37028  dfcnvrefrels2  37063  dfcnvrefrel2  37065  symrefref2  37098  lcv1  37576  lfl1dim  37656  lfl1dim2N  37657  paddasslem17  38372  dihglblem6  39876  dochvalr  39893  dochord3  39908  lpolconN  40023  lcfls1lem  40070  mapdffval  40162  mapdfval  40163  mapdsn2  40178  mapd0  40201  lspindp5  40306  mapdh8ab  40313  ismrcd1  41079  nacsfix  41093  setindtr  41406  hbtlem6  41514  oaabsb  41687  tfsconcatrnss  41743  naddwordnexlem4  41795  clcnvlem  42017  iunrelexpmin1  42102  iunrelexpmin2  42106  relexp0a  42110  cotrcltrcl  42119  trclimalb2  42120  cotrclrcl  42136  sbcheg  42173  clsk1indlem1  42439  isotone1  42442  isotone2  42443  ntrclsiso  42461  ntrclsk2  42462  k0004lem1  42541  k0004lem3  42543  scottelrankd  42649  mnuop123d  42664  mnuprdlem1  42674  mnuprdlem2  42675  mnuunid  42679  mnurndlem1  42683  ssdec  43420  iinssd  43463  iinssdf  43471  ssnnf1octb  43536  iooiinicc  43900  iooiinioc  43914  icccncfext  44248  fourierdlem41  44509  meaiininclem  44847  hoidmvlelem3  44958  hoidmvle  44961  opnvonmbllem1  44993  opnvonmbl  44995  iinhoiicclem  45034  smflim  45138  smflimsuplem7  45187  uspgrsprf  46168  iscnrm3r  47101  iscnrm3l  47104  setrecseq  47250  setrec1lem4  47255  setrec2fun  47257