Theorem sseq1d 3962

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseq12d  3964  eqsstrd  3965  ssiun2s  5007  disjxiun  5100  treq  5219  iunopeqop  5494  iunopeqopOLD  5495  dfpo2  6292  preddowncl  6328  funimass1  6614  feq1  6679  focofo  6801  fvmptss  6998  fvimacnvi  7043  fvimacnvALT  7048  knatar  7359  ovmptss  8093  fnsuppres  8192  frecseq123  8284  csbfrecsg  8286  frrlem1  8288  frrlem3  8290  frrlem4  8291  frrlem13  8300  frrdmcl  8310  fprresex  8312  dfrecs3  8364  oaordi  8538  oaword2  8545  oawordeulem  8546  omword1  8565  oewordri  8585  oeordsuc  8587  nnaordi  8611  nnawordex  8630  naddcllem  8669  naddunif  8687  ereq1  8709  elpm2r  8849  inficl  9401  fipwss  9405  dffi3  9407  hartogslem1  9520  inf3lema  9609  inf3lemd  9612  cantnfle  9656  cantnflem2  9675  ttrclselem1  9710  trcl  9713  tcmin  9724  rankr1ai  9788  rankxplim  9877  scottex  9914  scottexOLD  9915  scott0b  9918  scott0OLD  9919  scottexsOLD  9924  scott0bsOLD  9926  scottelrankd  9929  kardenOLD  9941  setrec1lem4  9952  setrec2fun  9954  cardne  10027  cardaleph  10149  ackbij2  10301  cflim2  10322  cfslb  10325  coftr  10332  fin23lem15  10393  fin23lem32  10403  fin23lem34  10405  fin23lem35  10406  fin23lem36  10407  fin23lem41  10411  isf32lem1  10412  itunitc1  10479  axdc3lem2  10510  ttukeylem1  10568  fpwwe2cbv  10696  fpwwe2lem2  10698  fpwwe2lem4  10700  fpwwe2  10709  fpwwecbv  10710  fpwwelem  10711  canthwelem  10716  canthwe  10717  pwfseqlem4  10728  wunex2  10804  wuncval2  10813  eltsk2g  10817  tskpwss  10818  inar1  10841  grothpw  10892  grothpwex  10893  axgroth6  10894  grothac  10896  peano5uzti  12770  fsuppmapnn0fiub0  14116  relexpnndm  15174  rtrclreclem4  15194  dfrtrcl2  15195  lo1o1  15679  o1lo1  15684  o1lo12  15685  lo1eq  15715  rlimeq  15716  isercoll  15815  prmreclem4  17077  vdwmc  17136  vdwlem1  17139  vdwlem2  17140  vdwlem12  17150  vdwlem13  17151  ramval  17166  ramz2  17182  ramub1lem1  17184  isacs2  17807  isacs1i  17811  mreacs  17812  acsfn  17813  rescabs  17988  ipole  18688  ipodrsima  18695  isacs5  18702  symgsssg  19661  psgnunilem5  19688  sylow1  19797  efgval2  19918  efgsfo  19933  frgpuplem  19966  gsumzf1o  20106  gsumzoppg  20138  dprdcntz  20204  islbs2  21412  frlmssuvc1  22080  frlmssuvc2  22081  frlmsslsp  22082  lindsenlbs  22137  ismhp  22441  pptbas  23306  pnfnei  23518  mnfnei  23519  iscnp  23535  iscnp4  23561  cnntr  23573  cnconst2  23581  cnpresti  23586  cnprest  23587  isreg  23630  isnrm  23633  isnrm2  23656  perfcls  23663  isreg2  23675  hauscmplem  23704  1stcfb  23743  1stcelcls  23760  1stccnp  23761  txbas  23866  ptbasfi  23880  xkoopn  23888  xkoccn  23918  txcnp  23919  ptcnplem  23920  txdis  23931  txdis1cn  23934  txtube  23939  txkgen  23951  xkohaus  23952  xkoptsub  23953  xkoco1cn  23956  xkoco2cn  23957  xkococnlem  23958  xkococn  23959  xkoinjcn  23986  kqreglem1  24040  kqreglem2  24041  kqnrmlem1  24042  kqnrmlem2  24043  reghmph  24092  nrmhmph  24093  trfil2  24186  ufileu  24218  elfm  24246  elfm2  24247  elfm3  24249  imaelfm  24250  rnelfm  24252  fmfnfmlem2  24254  fmfnfmlem4  24256  fmco  24260  elflim2  24263  flffbas  24294  lmflf  24304  txflf  24305  fclscf  24324  flimfnfcls  24327  cnextcn  24366  symgtgp  24405  ghmcnp  24414  qustgplem  24420  eltsms  24432  ustval  24502  ust0  24519  trust  24528  utoptop  24533  restutop  24536  restutopopn  24537  utopsnneiplem  24546  ucncn  24583  fmucnd  24590  cfilufg  24591  trcfilu  24592  neipcfilu  24594  blssps  24723  blss  24724  ssblex  24727  blin2  24728  metss2  24811  metrest  24823  metcnp3  24839  metustexhalf  24855  metustbl  24865  psmetutop  24866  xrsmopn  25112  recld2  25114  icccmplem1  25122  icccmplem2  25123  icccmp  25125  reconnlem2  25127  lebnumlem3  25264  lebnum  25265  xlebnum  25266  lebnumii  25267  nmhmcn  25421  cfilfval  25565  caubl  25609  caublcls  25610  bcthlem1  25625  bcth  25630  ovolfiniun  25802  ovoliunlem3  25805  ovoliun  25806  ovoliun2  25807  ovoliunnul  25808  voliunlem3  25853  dyadmax  25899  dyadmbllem  25900  dyadmbl  25901  opnmbllem  25902  ellimc2  26177  limcnlp  26178  ellimc3  26179  limcflf  26181  limciun  26194  cpnord  26235  lhop  26316  xrlimcnp  27278  cvxcl  27294  dchrval  27543  noetalem2  28081  madebdayim  28256  madebdaylemold  28266  madebday  28268  bdayle  28284  precsexlem8  28582  bdaypw2n0bndlem  28831  bdayfinbndcbv  28834  bdayfinbndlem1  28835  bdayfinbndlem2  28836  bdayfinbnd  28837  lnssplng  29252  ausgrumgri  29730  ausgrusgri  29731  nbgrval  29899  nbgrel  29903  nbumgrvtx  29909  nbgrnself  29922  uvtxel1  29959  wlkonl1iedg  30226  crctcshwlkn0lem6  30386  2wlkdlem10  30506  1wlkdlem4  30713  3wlkdlem6  30748  3wlkdlem10  30752  eupth2lem3lem4  30814  frcond1  30849  frgr1v  30854  nfrgr2v  30855  frgr3vlem1  30856  frgr3vlem2  30857  frgr3v  30858  4cycl2vnunb  30873  n4cyclfrgr  30874  isssp  31308  ubthlem1  31454  shmodi  31974  chsupid  31996  chsscon3  32084  spansncvi  32236  mdslmd1lem3  32911  mdslmd1lem4  32912  mdsymlem5  32991  dmdbr5ati  33006  dmdbr6ati  33007  dmdbr7ati  33008  ssiun2sf  33136  fpwrelmapffslem  33306  prodindf  33411  pwrssmgc  33543  fldgenval  33856  unitprodclb  33926  esplysply  34185  esplyfvaln  34188  esplyind  34189  resssra  34201  constrsscn  34354  constrextdg2lem  34362  constrextdg2  34363  txomap  34448  locfinreflem  34454  tpr2rico  34526  pnfneige0  34565  rrhre  34635  dya2icoseg2  34893  omsfval  34909  eulerpartlemt0  34984  eulerpartgbij  34987  eulerpartlemr  34989  eulerpartlemgs2  34995  eulerpartlemn  34996  eulerpart  34997  bnj517  35498  bnj1014  35574  bnj1015  35575  bnj1123  35599  bnj1125  35605  bnj1450  35663  bnj1452  35665  elscott  35719  elkarden  35796  cplgredgex  35874  kur14  35950  cvmliftlem15  36032  cvmlift2lem12  36048  cvmlift2lem13  36049  mclsval  36297  mclsax  36303  mclsppslem  36317  prodeq12sdv  36977  cbvsumdavw2  37054  cbvproddavw2  37055  opnrebl  37078  opnrebl2  37079  ivthALT  37093  neibastop2lem  37118  fnemeet1  37124  filnetlem1  37136  filnetlem4  37139  ttcmin  37254  dfttc2g  37264  bj-imdirval3  38073  bj-imdiridlem  38074  rdgssun  38269  lindsadd  38504  ptrecube  38506  poimirlem32  38538  opnmbllem0  38542  mblfinlem1  38543  mblfinlem2  38544  mblfinlem3  38545  ovoliunnfl  38548  ex-ovoliunnfl  38549  voliunnfl  38550  totbndbnd  38691  heibor1lem  38711  heiborlem10  38722  scottexf  39068  scott0f  39069  relcnveq2  39229  cnvref4  39250  dfcnvrefrels2  39508  dfcnvrefrel2  39510  elrelscnveq2  39529  symrefref2  39547  lcv1  40066  lfl1dim  40146  lfl1dim2N  40147  paddasslem17  40861  dihglblem6  42365  dochvalr  42382  dochord3  42397  lpolconN  42512  lcfls1lem  42559  mapdffval  42651  mapdfval  42652  mapdsn2  42667  mapd0  42690  lspindp5  42795  mapdh8ab  42802  primrootscoprbij  43120  aks6d1c2  43148  aks6d1c6lem3  43190  aks6d1c6lem5  43195  aks6d1c7lem1  43198  ismrcd1  43662  nacsfix  43676  setindtr  43984  hbtlem6  44089  oaabsb  44254  tfsconcatrnss  44310  naddwordnexlem4  44361  clcnvlem  44582  iunrelexpmin1  44667  iunrelexpmin2  44671  relexp0a  44675  cotrcltrcl  44684  trclimalb2  44685  cotrclrcl  44701  sbcheg  44738  clsk1indlem1  45004  isotone1  45007  isotone2  45008  ntrclsiso  45026  ntrclsk2  45027  k0004lem1  45106  k0004lem3  45108  mnuop123d  45205  mnuprdlem1  45215  mnuprdlem2  45216  mnuunid  45220  mnurndlem1  45224  modelaxreplem1  45920  modelaxreplem2  45921  modelaxrep  45923  ssdec  46046  iinssd  46089  iinssdf  46097  ssnnf1octb  46152  iooiinicc  46498  iooiinioc  46512  icccncfext  46841  fourierdlem41  47102  meaiininclem  47440  hoidmvlelem3  47551  hoidmvle  47554  opnvonmbllem1  47586  opnvonmbl  47588  iinhoiicclem  47627  smflim  47731  smflimsuplem7  47780  clnbgrval  48864  clnbgrel  48870  sclnbgrel  48889  isubgredg  48908  isubgruhgr  48910  uhgrimisgrgriclem  48972  uhgrimisgrgric  48973  clnbgrgrimlem  48975  clnbgrgrim  48976  isubgr3stgrlem7  49014  uspgrlimlem1  49030  uspgrlimlem2  49031  uspgrlimlem3  49032  uspgrlim  49034  pgnbgreunbgr  49167  uspgrsprf  49188  iinglb  49876  iscnrm3r  50000  iscnrm3l  50003  imassc  50205  setrecseq  50732