Theorem sseq1d 4040

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseq12d  4042  eqsstrd  4047  ssiun2s  5071  disjxiun  5163  treq  5291  iunopeqop  5540  dfpo2  6327  preddowncl  6364  funimass1  6660  feq1  6728  focofo  6847  fvmptss  7041  fvimacnvi  7085  fvimacnvALT  7090  knatar  7393  ovmptss  8134  fnsuppres  8232  frecseq123  8323  csbfrecsg  8325  frrlem1  8327  frrlem3  8329  frrlem4  8330  frrlem13  8339  frrdmcl  8349  fprresex  8351  wrecseq123OLD  8356  wfrlem1OLD  8364  wfrlem3OLD  8366  wfrdmclOLD  8373  wfrlem15OLD  8379  wfrlem17OLD  8381  dfrecs3  8428  dfrecs3OLD  8429  oaordi  8602  oaword2  8609  oawordeulem  8610  omword1  8629  oewordri  8648  oeordsuc  8650  nnaordi  8674  nnawordex  8693  naddcllem  8732  naddunif  8749  ereq1  8770  elpm2r  8903  inficl  9494  fipwss  9498  dffi3  9500  hartogslem1  9611  inf3lema  9693  inf3lemd  9696  cantnfle  9740  cantnflem2  9759  ttrclselem1  9794  trcl  9797  tcmin  9810  rankr1ai  9867  rankxplim  9948  scottex  9954  scott0  9955  scottexs  9956  scott0s  9957  karden  9964  cardne  10034  cardaleph  10158  ackbij2  10311  cflim2  10332  cfslb  10335  coftr  10342  fin23lem15  10403  fin23lem32  10413  fin23lem34  10415  fin23lem35  10416  fin23lem36  10417  fin23lem41  10421  isf32lem1  10422  itunitc1  10489  axdc3lem2  10520  ttukeylem1  10578  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwe2lem4  10703  fpwwe2  10712  fpwwecbv  10713  fpwwelem  10714  canthwelem  10719  canthwe  10720  pwfseqlem4  10731  wunex2  10807  wuncval2  10816  eltsk2g  10820  tskpwss  10821  inar1  10844  grothpw  10895  grothpwex  10896  axgroth6  10897  grothac  10899  peano5uzti  12733  fsuppmapnn0fiub0  14044  relexpnndm  15090  rtrclreclem4  15110  dfrtrcl2  15111  lo1o1  15578  o1lo1  15583  o1lo12  15584  lo1eq  15614  rlimeq  15615  isercoll  15716  prmreclem4  16966  vdwmc  17025  vdwlem1  17028  vdwlem2  17029  vdwlem12  17039  vdwlem13  17040  ramval  17055  ramz2  17071  ramub1lem1  17073  isacs2  17711  isacs1i  17715  mreacs  17716  acsfn  17717  rescabs  17896  rescabsOLD  17897  ipole  18604  ipodrsima  18611  isacs5  18618  symgsssg  19509  psgnunilem5  19536  sylow1  19645  efgval2  19766  efgsfo  19781  frgpuplem  19814  gsumzf1o  19954  gsumzoppg  19986  dprdcntz  20052  islbs2  21179  frlmssuvc1  21837  frlmssuvc2  21838  frlmsslsp  21839  ismhp  22167  pptbas  23036  pnfnei  23249  mnfnei  23250  iscnp  23266  iscnp4  23292  cnntr  23304  cnconst2  23312  cnpresti  23317  cnprest  23318  isreg  23361  isnrm  23364  isnrm2  23387  perfcls  23394  isreg2  23406  hauscmplem  23435  1stcfb  23474  1stcelcls  23490  1stccnp  23491  txbas  23596  ptbasfi  23610  xkoopn  23618  xkoccn  23648  txcnp  23649  ptcnplem  23650  txdis  23661  txdis1cn  23664  txtube  23669  txkgen  23681  xkohaus  23682  xkoptsub  23683  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  reghmph  23822  nrmhmph  23823  trfil2  23916  ufileu  23948  elfm  23976  elfm2  23977  elfm3  23979  imaelfm  23980  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  fmco  23990  elflim2  23993  flffbas  24024  lmflf  24034  txflf  24035  fclscf  24054  flimfnfcls  24057  cnextcn  24096  symgtgp  24135  ghmcnp  24144  qustgplem  24150  eltsms  24162  ustval  24232  ust0  24249  trust  24259  utoptop  24264  restutop  24267  restutopopn  24268  utopsnneiplem  24277  ucncn  24315  fmucnd  24322  cfilufg  24323  trcfilu  24324  neipcfilu  24326  blssps  24455  blss  24456  ssblex  24459  blin2  24460  metss2  24546  metrest  24558  metcnp3  24574  metustexhalf  24590  metustbl  24600  psmetutop  24601  xrsmopn  24853  recld2  24855  icccmplem1  24863  icccmplem2  24864  icccmp  24866  reconnlem2  24868  lebnumlem3  25014  lebnum  25015  xlebnum  25016  lebnumii  25017  nmhmcn  25172  cfilfval  25317  caubl  25361  caublcls  25362  bcthlem1  25377  bcth  25382  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  ovoliunnul  25561  voliunlem3  25606  dyadmax  25652  dyadmbllem  25653  dyadmbl  25654  opnmbllem  25655  ellimc2  25932  limcnlp  25933  ellimc3  25934  limcflf  25936  limciun  25949  cpnord  25991  lhop  26075  xrlimcnp  27029  cvxcl  27046  dchrval  27296  noetalem2  27805  madebdayim  27944  madebdaylemold  27954  madebday  27956  precsexlem8  28256  ausgrumgri  29202  ausgrusgri  29203  nbgrval  29371  nbgrel  29375  nbumgrvtx  29381  nbgrnself  29394  uvtxel1  29431  wlkonl1iedg  29701  crctcshwlkn0lem6  29848  2wlkdlem10  29968  1wlkdlem4  30172  3wlkdlem6  30197  3wlkdlem10  30201  eupth2lem3lem4  30263  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3vlem1  30305  frgr3vlem2  30306  frgr3v  30307  4cycl2vnunb  30322  n4cyclfrgr  30323  isssp  30756  ubthlem1  30902  shmodi  31422  chsupid  31444  chsscon3  31532  spansncvi  31684  mdslmd1lem3  32359  mdslmd1lem4  32360  mdsymlem5  32439  dmdbr5ati  32454  dmdbr6ati  32455  dmdbr7ati  32456  ssiun2sf  32582  fpwrelmapffslem  32746  pwrssmgc  32973  fldgenval  33279  unitprodclb  33382  resssra  33602  constrsscn  33730  txomap  33780  locfinreflem  33786  tpr2rico  33858  pnfneige0  33897  rrhre  33967  prodindf  33987  dya2icoseg2  34243  omsfval  34259  eulerpartlemt0  34334  eulerpartgbij  34337  eulerpartlemr  34339  eulerpartlemgs2  34345  eulerpartlemn  34346  eulerpart  34347  bnj517  34861  bnj1014  34937  bnj1015  34938  bnj1123  34962  bnj1125  34968  bnj1450  35026  bnj1452  35028  cplgredgex  35088  kur14  35184  cvmliftlem15  35266  cvmlift2lem12  35282  cvmlift2lem13  35283  mclsval  35531  mclsax  35537  mclsppslem  35551  prodeq12sdv  36184  cbvsumdavw2  36261  cbvproddavw2  36262  opnrebl  36286  opnrebl2  36287  ivthALT  36301  neibastop2lem  36326  fnemeet1  36332  filnetlem1  36344  filnetlem4  36347  bj-imdirval3  37150  bj-imdiridlem  37151  rdgssun  37344  lindsadd  37573  lindsenlbs  37575  ptrecube  37580  poimirlem32  37612  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  ovoliunnfl  37622  ex-ovoliunnfl  37623  voliunnfl  37624  totbndbnd  37749  heibor1lem  37769  heiborlem10  37780  scottexf  38128  scott0f  38129  relcnveq2  38279  cnvref4  38306  elrelscnveq2  38449  dfcnvrefrels2  38484  dfcnvrefrel2  38486  symrefref2  38519  lcv1  38997  lfl1dim  39077  lfl1dim2N  39078  paddasslem17  39793  dihglblem6  41297  dochvalr  41314  dochord3  41329  lpolconN  41444  lcfls1lem  41491  mapdffval  41583  mapdfval  41584  mapdsn2  41599  mapd0  41622  lspindp5  41727  mapdh8ab  41734  primrootscoprbij  42059  aks6d1c2  42087  aks6d1c6lem3  42129  aks6d1c6lem5  42134  aks6d1c7lem1  42137  ismrcd1  42654  nacsfix  42668  setindtr  42981  hbtlem6  43086  oaabsb  43256  tfsconcatrnss  43312  naddwordnexlem4  43363  clcnvlem  43585  iunrelexpmin1  43670  iunrelexpmin2  43674  relexp0a  43678  cotrcltrcl  43687  trclimalb2  43688  cotrclrcl  43704  sbcheg  43741  clsk1indlem1  44007  isotone1  44010  isotone2  44011  ntrclsiso  44029  ntrclsk2  44030  k0004lem1  44109  k0004lem3  44111  scottelrankd  44216  mnuop123d  44231  mnuprdlem1  44241  mnuprdlem2  44242  mnuunid  44246  mnurndlem1  44250  ssdec  44990  iinssd  45033  iinssdf  45041  ssnnf1octb  45101  iooiinicc  45460  iooiinioc  45474  icccncfext  45808  fourierdlem41  46069  meaiininclem  46407  hoidmvlelem3  46518  hoidmvle  46521  opnvonmbllem1  46553  opnvonmbl  46555  iinhoiicclem  46594  smflim  46698  smflimsuplem7  46747  clnbgrval  47696  clnbgrel  47701  sclnbgrel  47719  isubgruhgr  47738  uhgrimisgrgriclem  47782  uhgrimisgrgric  47783  clnbgrgrimlem  47785  clnbgrgrim  47786  uspgrlimlem1  47812  uspgrlimlem2  47813  uspgrlimlem3  47814  uspgrlim  47816  uspgrsprf  47869  iscnrm3r  48628  iscnrm3l  48631  setrecseq  48777  setrec1lem4  48782  setrec2fun  48784