Theorem sseq1d 3953

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseq12d  3955  eqsstrd  3960  ssiun2s  4979  disjxiun  5072  treq  5198  iunopeqop  5436  dfpo2  6203  preddowncl  6239  funimass1  6523  feq1  6590  focofo  6710  fvmptss  6896  fvimacnvi  6938  fvimacnvALT  6943  knatar  7237  ovmptss  7942  fnsuppres  8016  frecseq123  8107  csbfrecsg  8109  frrlem1  8111  frrlem3  8113  frrlem4  8114  frrlem13  8123  frrdmcl  8133  fprresex  8135  wrecseq123OLD  8140  wfrlem1OLD  8148  wfrlem3OLD  8150  wfrdmclOLD  8157  wfrlem15OLD  8163  wfrlem17OLD  8165  dfrecs3  8212  dfrecs3OLD  8213  oaordi  8386  oaword2  8393  oawordeulem  8394  omword1  8413  oewordri  8432  oeordsuc  8434  nnaordi  8458  nnawordex  8477  ereq1  8514  elpm2r  8642  inficl  9193  fipwss  9197  dffi3  9199  hartogslem1  9310  inf3lema  9391  inf3lemd  9394  cantnfle  9438  cantnflem2  9457  ttrclselem1  9492  trcl  9495  tcmin  9508  rankr1ai  9565  rankxplim  9646  scottex  9652  scott0  9653  scottexs  9654  scott0s  9655  karden  9662  cardne  9732  cardaleph  9854  ackbij2  10008  cflim2  10028  cfslb  10031  coftr  10038  fin23lem15  10099  fin23lem32  10109  fin23lem34  10111  fin23lem35  10112  fin23lem36  10113  fin23lem41  10117  isf32lem1  10118  itunitc1  10185  axdc3lem2  10216  ttukeylem1  10274  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwe2  10408  fpwwecbv  10409  fpwwelem  10410  canthwelem  10415  canthwe  10416  wunex2  10503  wuncval2  10512  eltsk2g  10516  tskpwss  10517  inar1  10540  grothpw  10591  grothpwex  10592  axgroth6  10593  grothac  10595  peano5uzti  12419  fsuppmapnn0fiub0  13722  relexpnndm  14761  rtrclreclem4  14781  dfrtrcl2  14782  lo1o1  15250  o1lo1  15255  o1lo12  15256  lo1eq  15286  rlimeq  15287  isercoll  15388  prmreclem4  16629  vdwmc  16688  vdwlem1  16691  vdwlem2  16692  vdwlem12  16702  vdwlem13  16703  ramval  16718  ramz2  16734  ramub1lem1  16736  isacs2  17371  isacs1i  17375  mreacs  17376  acsfn  17377  rescabs  17556  rescabsOLD  17557  ipole  18261  ipodrsima  18268  isacs5  18275  symgsssg  19084  psgnunilem5  19111  sylow1  19217  efgval2  19339  efgsfo  19354  frgpuplem  19387  gsumzf1o  19522  gsumzoppg  19554  dprdcntz  19620  islbs2  20425  frlmssuvc1  21010  frlmssuvc2  21011  frlmsslsp  21012  ismhp  21340  pptbas  22167  pnfnei  22380  mnfnei  22381  iscnp  22397  iscnp4  22423  cnntr  22435  cnconst2  22443  cnpresti  22448  cnprest  22449  isreg  22492  isnrm  22495  isnrm2  22518  perfcls  22525  isreg2  22537  hauscmplem  22566  1stcfb  22605  1stcelcls  22621  1stccnp  22622  txbas  22727  ptbasfi  22741  xkoopn  22749  xkoccn  22779  txcnp  22780  ptcnplem  22781  txdis  22792  txdis1cn  22795  txtube  22800  txkgen  22812  xkohaus  22813  xkoptsub  22814  xkoco1cn  22817  xkoco2cn  22818  xkococnlem  22819  xkococn  22820  xkoinjcn  22847  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  reghmph  22953  nrmhmph  22954  trfil2  23047  ufileu  23079  elfm  23107  elfm2  23108  elfm3  23110  imaelfm  23111  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem4  23117  fmco  23121  elflim2  23124  flffbas  23155  lmflf  23165  txflf  23166  fclscf  23185  flimfnfcls  23188  cnextcn  23227  symgtgp  23266  ghmcnp  23275  qustgplem  23281  eltsms  23293  ustval  23363  ust0  23380  trust  23390  utoptop  23395  restutop  23398  restutopopn  23399  utopsnneiplem  23408  ucncn  23446  fmucnd  23453  cfilufg  23454  trcfilu  23455  neipcfilu  23457  blssps  23586  blss  23587  ssblex  23590  blin2  23591  metss2  23677  metrest  23689  metcnp3  23705  metustexhalf  23721  metustbl  23731  psmetutop  23732  xrsmopn  23984  recld2  23986  icccmplem1  23994  icccmplem2  23995  icccmp  23997  reconnlem2  23999  lebnumlem3  24135  lebnum  24136  xlebnum  24137  lebnumii  24138  nmhmcn  24292  cfilfval  24437  caubl  24481  caublcls  24482  bcthlem1  24497  bcth  24502  ovolfiniun  24674  ovoliunlem3  24677  ovoliun  24678  ovoliun2  24679  ovoliunnul  24680  voliunlem3  24725  dyadmax  24771  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  ellimc2  25050  limcnlp  25051  ellimc3  25052  limcflf  25054  limciun  25067  cpnord  25108  lhop  25189  xrlimcnp  26127  cvxcl  26143  dchrval  26391  ausgrumgri  27546  ausgrusgri  27547  nbgrval  27712  nbgrel  27716  nbumgrvtx  27722  nbgrnself  27735  uvtxel1  27772  wlkonl1iedg  28042  crctcshwlkn0lem6  28189  2wlkdlem10  28309  1wlkdlem4  28513  3wlkdlem6  28538  3wlkdlem10  28542  eupth2lem3lem4  28604  frcond1  28639  frgr1v  28644  nfrgr2v  28645  frgr3vlem1  28646  frgr3vlem2  28647  frgr3v  28648  4cycl2vnunb  28663  n4cyclfrgr  28664  isssp  29095  ubthlem1  29241  shmodi  29761  chsupid  29783  chsscon3  29871  spansncvi  30023  mdslmd1lem3  30698  mdslmd1lem4  30699  mdsymlem5  30778  dmdbr5ati  30793  dmdbr6ati  30794  dmdbr7ati  30795  ssiun2sf  30908  fpwrelmapffslem  31076  pwrssmgc  31287  txomap  31793  locfinreflem  31799  tpr2rico  31871  pnfneige0  31910  rrhre  31980  prodindf  32000  dya2icoseg2  32254  omsfval  32270  eulerpartlemt0  32345  eulerpartgbij  32348  eulerpartlemr  32350  eulerpartlemgs2  32356  eulerpartlemn  32357  eulerpart  32358  bnj517  32874  bnj1014  32950  bnj1015  32951  bnj1123  32975  bnj1125  32981  bnj1450  33039  bnj1452  33041  cplgredgex  33091  kur14  33187  cvmliftlem15  33269  cvmlift2lem12  33285  cvmlift2lem13  33286  mclsval  33534  mclsax  33540  mclsppslem  33554  naddcllem  33840  noetalem2  33954  madebdayim  34079  madebdaylemold  34087  madebday  34089  opnrebl  34518  opnrebl2  34519  ivthALT  34533  neibastop2lem  34558  fnemeet1  34564  filnetlem1  34576  filnetlem4  34579  bj-imdirval3  35364  bj-imdiridlem  35365  rdgssun  35558  lindsadd  35779  lindsenlbs  35781  ptrecube  35786  poimirlem32  35818  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  ovoliunnfl  35828  ex-ovoliunnfl  35829  voliunnfl  35830  totbndbnd  35956  heibor1lem  35976  heiborlem10  35987  scottexf  36335  scott0f  36336  relcnveq2  36465  elrelscnveq2  36618  dfcnvrefrels2  36651  dfcnvrefrel2  36653  symrefref2  36684  lcv1  37062  lfl1dim  37142  lfl1dim2N  37143  paddasslem17  37857  dihglblem6  39361  dochvalr  39378  dochord3  39393  lpolconN  39508  lcfls1lem  39555  mapdffval  39647  mapdfval  39648  mapdsn2  39663  mapd0  39686  lspindp5  39791  mapdh8ab  39798  ismrcd1  40527  nacsfix  40541  setindtr  40853  hbtlem6  40961  clcnvlem  41238  iunrelexpmin1  41323  iunrelexpmin2  41327  relexp0a  41331  cotrcltrcl  41340  trclimalb2  41341  cotrclrcl  41357  sbcheg  41394  clsk1indlem1  41662  isotone1  41665  isotone2  41666  ntrclsiso  41684  ntrclsk2  41685  k0004lem1  41764  k0004lem3  41766  scottelrankd  41872  mnuop123d  41887  mnuprdlem1  41897  mnuprdlem2  41898  mnuunid  41902  mnurndlem1  41906  ssdec  42645  iinssd  42687  iinssdf  42695  ssnnf1octb  42740  iooiinicc  43087  iooiinioc  43101  icccncfext  43435  fourierdlem41  43696  meaiininclem  44031  hoidmvlelem3  44142  hoidmvle  44145  opnvonmbllem1  44177  opnvonmbl  44179  iinhoiicclem  44218  smflim  44322  smflimsuplem7  44370  uspgrsprf  45319  iscnrm3r  46253  iscnrm3l  46256  setrecseq  46402  setrec1lem4  46407  setrec2fun  46409