Theorem sseq1d 4000

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ⊆ wss 3938

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sseq12d  4002  eqsstrd  4007  ssiun2s  4974  disjxiun  5065  treq  5180  iunopeqop  5413  preddowncl  6177  funimass1  6438  feq1  6497  fvmptss  6782  fvimacnvi  6824  fvimacnvALT  6829  knatar  7112  ovmptss  7790  fnsuppres  7859  imacosuppOLD  7877  wrecseq123  7950  wfrlem1  7956  wfrlem3  7958  wfrdmcl  7965  wfrlem15  7971  wfrlem17  7973  dfrecs3  8011  oaordi  8174  oaword2  8181  oawordeulem  8182  omword1  8201  oewordri  8220  oeordsuc  8222  nnaordi  8246  nnawordex  8265  ereq1  8298  elpm2r  8426  inficl  8891  fipwss  8895  dffi3  8897  hartogslem1  9008  inf3lema  9089  inf3lemd  9092  cantnfle  9136  cantnflem2  9155  trcl  9172  tcmin  9185  rankr1ai  9229  rankxplim  9310  scottex  9316  scott0  9317  scottexs  9318  scott0s  9319  karden  9326  cardne  9396  cardaleph  9517  ackbij2  9667  cflim2  9687  cfslb  9690  coftr  9697  fin23lem15  9758  fin23lem32  9768  fin23lem34  9770  fin23lem35  9771  fin23lem36  9772  fin23lem41  9776  isf32lem1  9777  itunitc1  9844  axdc3lem2  9875  ttukeylem1  9933  fpwwe2cbv  10054  fpwwe2lem2  10056  fpwwe2  10067  fpwwecbv  10068  fpwwelem  10069  canthwelem  10074  canthwe  10075  wunex2  10162  wuncval2  10171  eltsk2g  10175  tskpwss  10176  inar1  10199  grothpw  10250  grothpwex  10251  axgroth6  10252  grothac  10254  peano5uzti  12075  fsuppmapnn0fiub0  13364  relexpnndm  14402  rtrclreclem4  14422  dfrtrcl2  14423  lo1o1  14891  o1lo1  14896  o1lo12  14897  lo1eq  14927  rlimeq  14928  isercoll  15026  prmreclem4  16257  vdwmc  16316  vdwlem1  16319  vdwlem2  16320  vdwlem12  16330  vdwlem13  16331  ramval  16346  ramz2  16362  ramub1lem1  16364  isacs2  16926  isacs1i  16930  mreacs  16931  acsfn  16932  rescabs  17105  ipole  17770  ipodrsima  17777  isacs5  17784  symgsssg  18597  psgnunilem5  18624  sylow1  18730  efgval2  18852  efgsfo  18867  frgpuplem  18900  gsumzf1o  19034  gsumzoppg  19066  dprdcntz  19132  islbs2  19928  ismhp  20336  frlmssuvc1  20940  frlmssuvc2  20941  frlmsslsp  20942  pptbas  21618  pnfnei  21830  mnfnei  21831  iscnp  21847  iscnp4  21873  cnntr  21885  cnconst2  21893  cnpresti  21898  cnprest  21899  isreg  21942  isnrm  21945  isnrm2  21968  perfcls  21975  isreg2  21987  hauscmplem  22016  1stcfb  22055  1stcelcls  22071  1stccnp  22072  txbas  22177  ptbasfi  22191  xkoopn  22199  xkoccn  22229  txcnp  22230  ptcnplem  22231  txdis  22242  txdis1cn  22245  txtube  22250  txkgen  22262  xkohaus  22263  xkoptsub  22264  xkoco1cn  22267  xkoco2cn  22268  xkococnlem  22269  xkococn  22270  xkoinjcn  22297  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  reghmph  22403  nrmhmph  22404  trfil2  22497  ufileu  22529  elfm  22557  elfm2  22558  elfm3  22560  imaelfm  22561  rnelfm  22563  fmfnfmlem2  22565  fmfnfmlem4  22567  fmco  22571  elflim2  22574  flffbas  22605  lmflf  22615  txflf  22616  fclscf  22635  flimfnfcls  22638  cnextcn  22677  symgtgp  22716  ghmcnp  22725  qustgplem  22731  eltsms  22743  ustval  22813  ust0  22830  trust  22840  utoptop  22845  restutop  22848  restutopopn  22849  utopsnneiplem  22858  ucncn  22896  fmucnd  22903  cfilufg  22904  trcfilu  22905  neipcfilu  22907  blssps  23036  blss  23037  ssblex  23040  blin2  23041  metss2  23124  metrest  23136  metcnp3  23152  metustexhalf  23168  metustbl  23178  psmetutop  23179  xrsmopn  23422  recld2  23424  icccmplem1  23432  icccmplem2  23433  icccmp  23435  reconnlem2  23437  lebnumlem3  23569  lebnum  23570  xlebnum  23571  lebnumii  23572  nmhmcn  23726  cfilfval  23869  caubl  23913  caublcls  23914  bcthlem1  23929  bcth  23934  ovolfiniun  24104  ovoliunlem3  24107  ovoliun  24108  ovoliun2  24109  ovoliunnul  24110  voliunlem3  24155  dyadmax  24201  dyadmbllem  24202  dyadmbl  24203  opnmbllem  24204  ellimc2  24477  limcnlp  24478  ellimc3  24479  limcflf  24481  limciun  24494  cpnord  24534  lhop  24615  xrlimcnp  25548  cvxcl  25564  dchrval  25812  ausgrumgri  26954  ausgrusgri  26955  nbgrval  27120  nbgrel  27124  nbumgrvtx  27130  nbgrnself  27143  uvtxel1  27180  wlkonl1iedg  27449  crctcshwlkn0lem6  27595  2wlkdlem10  27716  1wlkdlem4  27921  3wlkdlem6  27946  3wlkdlem10  27950  eupth2lem3lem4  28012  frcond1  28047  frgr1v  28052  nfrgr2v  28053  frgr3vlem1  28054  frgr3vlem2  28055  frgr3v  28056  4cycl2vnunb  28071  n4cyclfrgr  28072  isssp  28503  ubthlem1  28649  shmodi  29169  chsupid  29191  chsscon3  29279  spansncvi  29431  mdslmd1lem3  30106  mdslmd1lem4  30107  mdsymlem5  30186  dmdbr5ati  30201  dmdbr6ati  30202  dmdbr7ati  30203  ssiun2sf  30313  fpwrelmapffslem  30470  txomap  31100  locfinreflem  31106  tpr2rico  31157  pnfneige0  31196  rrhre  31264  prodindf  31284  dya2icoseg2  31538  omsfval  31554  eulerpartlemt0  31629  eulerpartgbij  31632  eulerpartlemr  31634  eulerpartlemgs2  31640  eulerpartlemn  31641  eulerpart  31642  bnj517  32159  bnj1014  32235  bnj1015  32236  bnj1123  32260  bnj1125  32266  bnj1450  32324  bnj1452  32326  cplgredgex  32369  kur14  32465  cvmliftlem15  32547  cvmlift2lem12  32563  cvmlift2lem13  32564  mclsval  32812  mclsax  32818  mclsppslem  32832  dfpo2  32993  trpredlem1  33068  trpredmintr  33072  frecseq123  33121  frrlem1  33125  frrlem3  33127  frrlem4  33128  frrlem13  33137  noetalem5  33223  opnrebl  33670  opnrebl2  33671  ivthALT  33685  neibastop2lem  33710  fnemeet1  33716  filnetlem1  33728  filnetlem4  33731  bj-imdirval3  34476  csbwrecsg  34610  rdgssun  34661  lindsadd  34887  lindsenlbs  34889  ptrecube  34894  poimirlem32  34926  opnmbllem0  34930  mblfinlem1  34931  mblfinlem2  34932  mblfinlem3  34933  ovoliunnfl  34936  ex-ovoliunnfl  34937  voliunnfl  34938  totbndbnd  35069  heibor1lem  35089  heiborlem10  35100  scottexf  35448  scott0f  35449  relcnveq2  35582  elrelscnveq2  35735  dfcnvrefrels2  35768  dfcnvrefrel2  35770  symrefref2  35801  lcv1  36179  lfl1dim  36259  lfl1dim2N  36260  paddasslem17  36974  dihglblem6  38478  dochvalr  38495  dochord3  38510  lpolconN  38625  lcfls1lem  38672  mapdffval  38764  mapdfval  38765  mapdsn2  38780  mapd0  38803  lspindp5  38908  mapdh8ab  38915  ismrcd1  39302  nacsfix  39316  setindtr  39628  hbtlem6  39736  clcnvlem  39990  iunrelexpmin1  40060  iunrelexpmin2  40064  relexp0a  40068  cotrcltrcl  40077  trclimalb2  40078  cotrclrcl  40094  sbcheg  40132  clsk1indlem1  40402  isotone1  40405  isotone2  40406  ntrclsiso  40424  ntrclsk2  40425  k0004lem1  40504  k0004lem3  40506  scottelrankd  40590  mnuop123d  40605  mnuprdlem1  40615  mnuprdlem2  40616  mnuunid  40620  mnurndlem1  40624  ssdec  41361  iinssd  41404  iinssdf  41415  ssnnf1octb  41463  iooiinicc  41825  iooiinioc  41839  icccncfext  42177  fourierdlem41  42440  meaiininclem  42775  hoidmvlelem3  42886  hoidmvle  42889  opnvonmbllem1  42921  opnvonmbl  42923  iinhoiicclem  42962  smflim  43060  smflimsuplem7  43107  uspgrsprf  44028  setrecseq  44795  setrec1lem4  44800  setrec2fun  44802