Theorem sseq1d 3995

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  sseq12d  3997  eqsstrd  3998  ssiun2s  5029  disjxiun  5121  treq  5242  iunopeqop  5501  dfpo2  6290  preddowncl  6326  funimass1  6623  f1imadifssran  6627  feq1  6691  focofo  6808  fvmptss  7003  fvimacnvi  7047  fvimacnvALT  7052  knatar  7355  ovmptss  8097  fnsuppres  8195  frecseq123  8286  csbfrecsg  8288  frrlem1  8290  frrlem3  8292  frrlem4  8293  frrlem13  8302  frrdmcl  8312  fprresex  8314  wrecseq123OLD  8319  wfrlem1OLD  8327  wfrlem3OLD  8329  wfrdmclOLD  8336  wfrlem15OLD  8342  wfrlem17OLD  8344  dfrecs3  8391  dfrecs3OLD  8392  oaordi  8563  oaword2  8570  oawordeulem  8571  omword1  8590  oewordri  8609  oeordsuc  8611  nnaordi  8635  nnawordex  8654  naddcllem  8693  naddunif  8710  ereq1  8731  elpm2r  8864  inficl  9442  fipwss  9446  dffi3  9448  hartogslem1  9561  inf3lema  9643  inf3lemd  9646  cantnfle  9690  cantnflem2  9709  ttrclselem1  9744  trcl  9747  tcmin  9760  rankr1ai  9817  rankxplim  9898  scottex  9904  scott0  9905  scottexs  9906  scott0s  9907  karden  9914  cardne  9984  cardaleph  10108  ackbij2  10261  cflim2  10282  cfslb  10285  coftr  10292  fin23lem15  10353  fin23lem32  10363  fin23lem34  10365  fin23lem35  10366  fin23lem36  10367  fin23lem41  10371  isf32lem1  10372  itunitc1  10439  axdc3lem2  10470  ttukeylem1  10528  fpwwe2cbv  10649  fpwwe2lem2  10651  fpwwe2lem4  10653  fpwwe2  10662  fpwwecbv  10663  fpwwelem  10664  canthwelem  10669  canthwe  10670  pwfseqlem4  10681  wunex2  10757  wuncval2  10766  eltsk2g  10770  tskpwss  10771  inar1  10794  grothpw  10845  grothpwex  10846  axgroth6  10847  grothac  10849  peano5uzti  12688  fsuppmapnn0fiub0  14016  relexpnndm  15065  rtrclreclem4  15085  dfrtrcl2  15086  lo1o1  15553  o1lo1  15558  o1lo12  15559  lo1eq  15589  rlimeq  15590  isercoll  15689  prmreclem4  16944  vdwmc  17003  vdwlem1  17006  vdwlem2  17007  vdwlem12  17017  vdwlem13  17018  ramval  17033  ramz2  17049  ramub1lem1  17051  isacs2  17670  isacs1i  17674  mreacs  17675  acsfn  17676  rescabs  17851  ipole  18549  ipodrsima  18556  isacs5  18563  symgsssg  19453  psgnunilem5  19480  sylow1  19589  efgval2  19710  efgsfo  19725  frgpuplem  19758  gsumzf1o  19898  gsumzoppg  19930  dprdcntz  19996  islbs2  21120  frlmssuvc1  21759  frlmssuvc2  21760  frlmsslsp  21761  ismhp  22083  pptbas  22951  pnfnei  23163  mnfnei  23164  iscnp  23180  iscnp4  23206  cnntr  23218  cnconst2  23226  cnpresti  23231  cnprest  23232  isreg  23275  isnrm  23278  isnrm2  23301  perfcls  23308  isreg2  23320  hauscmplem  23349  1stcfb  23388  1stcelcls  23404  1stccnp  23405  txbas  23510  ptbasfi  23524  xkoopn  23532  xkoccn  23562  txcnp  23563  ptcnplem  23564  txdis  23575  txdis1cn  23578  txtube  23583  txkgen  23595  xkohaus  23596  xkoptsub  23597  xkoco1cn  23600  xkoco2cn  23601  xkococnlem  23602  xkococn  23603  xkoinjcn  23630  kqreglem1  23684  kqreglem2  23685  kqnrmlem1  23686  kqnrmlem2  23687  reghmph  23736  nrmhmph  23737  trfil2  23830  ufileu  23862  elfm  23890  elfm2  23891  elfm3  23893  imaelfm  23894  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  fmco  23904  elflim2  23907  flffbas  23938  lmflf  23948  txflf  23949  fclscf  23968  flimfnfcls  23971  cnextcn  24010  symgtgp  24049  ghmcnp  24058  qustgplem  24064  eltsms  24076  ustval  24146  ust0  24163  trust  24173  utoptop  24178  restutop  24181  restutopopn  24182  utopsnneiplem  24191  ucncn  24228  fmucnd  24235  cfilufg  24236  trcfilu  24237  neipcfilu  24239  blssps  24368  blss  24369  ssblex  24372  blin2  24373  metss2  24456  metrest  24468  metcnp3  24484  metustexhalf  24500  metustbl  24510  psmetutop  24511  xrsmopn  24757  recld2  24759  icccmplem1  24767  icccmplem2  24768  icccmp  24770  reconnlem2  24772  lebnumlem3  24918  lebnum  24919  xlebnum  24920  lebnumii  24921  nmhmcn  25076  cfilfval  25221  caubl  25265  caublcls  25266  bcthlem1  25281  bcth  25286  ovolfiniun  25459  ovoliunlem3  25462  ovoliun  25463  ovoliun2  25464  ovoliunnul  25465  voliunlem3  25510  dyadmax  25556  dyadmbllem  25557  dyadmbl  25558  opnmbllem  25559  ellimc2  25835  limcnlp  25836  ellimc3  25837  limcflf  25839  limciun  25852  cpnord  25894  lhop  25978  xrlimcnp  26935  cvxcl  26952  dchrval  27202  noetalem2  27711  madebdayim  27856  madebdaylemold  27866  madebday  27868  precsexlem8  28173  ausgrumgri  29151  ausgrusgri  29152  nbgrval  29320  nbgrel  29324  nbumgrvtx  29330  nbgrnself  29343  uvtxel1  29380  wlkonl1iedg  29650  crctcshwlkn0lem6  29802  2wlkdlem10  29922  1wlkdlem4  30126  3wlkdlem6  30151  3wlkdlem10  30155  eupth2lem3lem4  30217  frcond1  30252  frgr1v  30257  nfrgr2v  30258  frgr3vlem1  30259  frgr3vlem2  30260  frgr3v  30261  4cycl2vnunb  30276  n4cyclfrgr  30277  isssp  30710  ubthlem1  30856  shmodi  31376  chsupid  31398  chsscon3  31486  spansncvi  31638  mdslmd1lem3  32313  mdslmd1lem4  32314  mdsymlem5  32393  dmdbr5ati  32408  dmdbr6ati  32409  dmdbr7ati  32410  ssiun2sf  32545  fpwrelmapffslem  32714  prodindf  32845  pwrssmgc  32985  fldgenval  33311  unitprodclb  33409  resssra  33632  constrsscn  33779  constrextdg2lem  33787  constrextdg2  33788  txomap  33870  locfinreflem  33876  tpr2rico  33948  pnfneige0  33987  rrhre  34057  dya2icoseg2  34315  omsfval  34331  eulerpartlemt0  34406  eulerpartgbij  34409  eulerpartlemr  34411  eulerpartlemgs2  34417  eulerpartlemn  34418  eulerpart  34419  bnj517  34921  bnj1014  34997  bnj1015  34998  bnj1123  35022  bnj1125  35028  bnj1450  35086  bnj1452  35088  cplgredgex  35148  kur14  35243  cvmliftlem15  35325  cvmlift2lem12  35341  cvmlift2lem13  35342  mclsval  35590  mclsax  35596  mclsppslem  35610  prodeq12sdv  36241  cbvsumdavw2  36318  cbvproddavw2  36319  opnrebl  36343  opnrebl2  36344  ivthALT  36358  neibastop2lem  36383  fnemeet1  36389  filnetlem1  36401  filnetlem4  36404  bj-imdirval3  37207  bj-imdiridlem  37208  rdgssun  37401  lindsadd  37642  lindsenlbs  37644  ptrecube  37649  poimirlem32  37681  opnmbllem0  37685  mblfinlem1  37686  mblfinlem2  37687  mblfinlem3  37688  ovoliunnfl  37691  ex-ovoliunnfl  37692  voliunnfl  37693  totbndbnd  37818  heibor1lem  37838  heiborlem10  37849  scottexf  38197  scott0f  38198  relcnveq2  38346  cnvref4  38373  elrelscnveq2  38516  dfcnvrefrels2  38551  dfcnvrefrel2  38553  symrefref2  38586  lcv1  39064  lfl1dim  39144  lfl1dim2N  39145  paddasslem17  39860  dihglblem6  41364  dochvalr  41381  dochord3  41396  lpolconN  41511  lcfls1lem  41558  mapdffval  41650  mapdfval  41651  mapdsn2  41666  mapd0  41689  lspindp5  41794  mapdh8ab  41801  primrootscoprbij  42120  aks6d1c2  42148  aks6d1c6lem3  42190  aks6d1c6lem5  42195  aks6d1c7lem1  42198  ismrcd1  42696  nacsfix  42710  setindtr  43023  hbtlem6  43128  oaabsb  43293  tfsconcatrnss  43349  naddwordnexlem4  43400  clcnvlem  43622  iunrelexpmin1  43707  iunrelexpmin2  43711  relexp0a  43715  cotrcltrcl  43724  trclimalb2  43725  cotrclrcl  43741  sbcheg  43778  clsk1indlem1  44044  isotone1  44047  isotone2  44048  ntrclsiso  44066  ntrclsk2  44067  k0004lem1  44146  k0004lem3  44148  scottelrankd  44246  mnuop123d  44261  mnuprdlem1  44271  mnuprdlem2  44272  mnuunid  44276  mnurndlem1  44280  modelaxreplem1  44978  modelaxreplem2  44979  modelaxrep  44981  ssdec  45092  iinssd  45135  iinssdf  45143  ssnnf1octb  45198  iooiinicc  45551  iooiinioc  45565  icccncfext  45896  fourierdlem41  46157  meaiininclem  46495  hoidmvlelem3  46606  hoidmvle  46609  opnvonmbllem1  46641  opnvonmbl  46643  iinhoiicclem  46682  smflim  46786  smflimsuplem7  46835  clnbgrval  47816  clnbgrel  47822  sclnbgrel  47840  isubgredg  47859  isubgruhgr  47861  uhgrimisgrgriclem  47923  uhgrimisgrgric  47924  clnbgrgrimlem  47926  clnbgrgrim  47927  isubgr3stgrlem7  47964  uspgrlimlem1  47980  uspgrlimlem2  47981  uspgrlimlem3  47982  uspgrlim  47984  uspgrsprf  48101  iinglb  48780  iscnrm3r  48902  iscnrm3l  48905  imassc  49073  setrecseq  49529  setrec1lem4  49534  setrec2fun  49536