Theorem sseq1d 3939

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12d  3941  eqsstrd  3942  ssiun2s  5006  disjxiun  5099  treq  5218  iunopeqop  5493  iunopeqopOLD  5494  dfpo2  6299  preddowncl  6335  funimass1  6622  feq1  6687  focofo  6809  fvmptss  7006  fvimacnvi  7051  fvimacnvALT  7056  knatar  7367  ovmptssOLD  8105  fnsuppres  8211  frecseq123  8303  csbfrecsg  8305  frrlem1  8307  frrlem3  8309  frrlem4  8310  frrlem13  8319  frrdmcl  8329  fprresex  8331  dfrecs3  8383  oaordi  8557  oaword2  8564  oawordeulem  8565  omword1  8584  oewordri  8604  oeordsuc  8606  nnaordi  8630  nnawordex  8649  naddcllem  8688  naddunif  8706  ereq1  8728  elpm2r  8868  inficl  9420  fipwss  9424  dffi3  9426  hartogslem1  9539  inf3lema  9628  inf3lemd  9631  cantnfle  9675  cantnflem2  9694  ttrclselem1  9729  trcl  9732  tcmin  9743  rankr1ai  9809  rankxplim  9899  scottex  9936  scottexOLD  9937  scott0b  9940  scott0OLD  9941  scottexsOLD  9946  scott0bsOLD  9948  scottelrankd  9951  kardenOLD  9963  setrec1lem4  9974  setrec2fun  9976  cardne  10049  cardaleph  10171  ackbij2  10323  cflim2  10344  cfslb  10347  coftr  10354  fin23lem15  10415  fin23lem32  10425  fin23lem34  10427  fin23lem35  10428  fin23lem36  10429  fin23lem41  10433  isf32lem1  10434  itunitc1  10501  axdc3lem2  10532  ttukeylem1  10590  fpwwe2cbv  10718  fpwwe2lem2  10720  fpwwe2lem4  10722  fpwwe2  10731  fpwwecbv  10732  fpwwelem  10733  canthwelem  10738  canthwe  10739  pwfseqlem4  10750  wunex2  10826  wuncval2  10835  eltsk2g  10839  tskpwss  10840  inar1  10863  grothpw  10914  grothpwex  10915  axgroth6  10916  grothac  10918  peano5uzti  12792  fsuppmapnn0fiub0  14139  relexpnndm  15199  rtrclreclem4  15219  dfrtrcl2  15220  lo1o1  15704  o1lo1  15709  o1lo12  15710  lo1eq  15740  rlimeq  15741  isercoll  15840  prmreclem4  17102  vdwmc  17161  vdwlem1  17164  vdwlem2  17165  vdwlem12  17175  vdwlem13  17176  ramval  17191  ramz2  17207  ramub1lem1  17209  isacs2  17832  isacs1i  17836  mreacs  17837  acsfn  17838  rescabs  18013  ipole  18713  ipodrsima  18720  isacs5  18727  symgsssg  19686  psgnunilem5  19713  sylow1  19822  efgval2  19943  efgsfo  19958  frgpuplem  19991  gsumzf1o  20131  gsumzoppg  20163  dprdcntz  20229  islbs2  21437  frlmssuvc1  22105  frlmssuvc2  22106  frlmsslsp  22107  lindsenlbs  22162  ismhp  22466  pptbas  23331  pnfnei  23543  mnfnei  23544  iscnp  23560  iscnp4  23586  cnntr  23598  cnconst2  23606  cnpresti  23611  cnprest  23612  isreg  23655  isnrm  23658  isnrm2  23681  perfcls  23688  isreg2  23700  hauscmplem  23729  1stcfb  23768  1stcelcls  23785  1stccnp  23786  txbas  23891  ptbasfi  23905  xkoopn  23913  xkoccn  23943  txcnp  23944  ptcnplem  23945  txdis  23956  txdis1cn  23959  txtube  23964  txkgen  23976  xkohaus  23977  xkoptsub  23978  xkoco1cn  23981  xkoco2cn  23982  xkococnlem  23983  xkococn  23984  xkoinjcn  24011  kqreglem1  24065  kqreglem2  24066  kqnrmlem1  24067  kqnrmlem2  24068  reghmph  24117  nrmhmph  24118  trfil2  24211  ufileu  24243  elfm  24271  elfm2  24272  elfm3  24274  imaelfm  24275  rnelfm  24277  fmfnfmlem2  24279  fmfnfmlem4  24281  fmco  24285  elflim2  24288  flffbas  24319  lmflf  24329  txflf  24330  fclscf  24349  flimfnfcls  24352  cnextcn  24391  symgtgp  24430  ghmcnp  24439  qustgplem  24445  eltsms  24457  ustval  24527  ust0  24544  trust  24553  utoptop  24558  restutop  24561  restutopopn  24562  utopsnneiplem  24571  ucncn  24608  fmucnd  24615  cfilufg  24616  trcfilu  24617  neipcfilu  24619  blssps  24748  blss  24749  ssblex  24752  blin2  24753  metss2  24836  metrest  24848  metcnp3  24864  metustexhalf  24880  metustbl  24890  psmetutop  24891  xrsmopn  25137  recld2  25139  icccmplem1  25147  icccmplem2  25148  icccmp  25150  reconnlem2  25152  lebnumlem3  25289  lebnum  25290  xlebnum  25291  lebnumii  25292  nmhmcn  25446  cfilfval  25590  caubl  25634  caublcls  25635  bcthlem1  25650  bcth  25655  ovolfiniun  25827  ovoliunlem3  25830  ovoliun  25831  ovoliun2  25832  ovoliunnul  25833  voliunlem3  25878  dyadmax  25924  dyadmbllem  25925  dyadmbl  25926  opnmbllem  25927  ellimc2  26202  limcnlp  26203  ellimc3  26204  limcflf  26206  limciun  26219  cpnord  26260  lhop  26341  xrlimcnp  27301  cvxcl  27317  dchrval  27566  noetalem2  28104  madebdayim  28279  madebdaylemold  28289  madebday  28291  bdayle  28307  precsexlem8  28605  bdaypw2n0bndlem  28854  bdayfinbndcbv  28857  bdayfinbndlem1  28858  bdayfinbndlem2  28859  bdayfinbnd  28860  lnssplng  29275  ausgrumgri  29753  ausgrusgri  29754  nbgrval  29922  nbgrel  29926  nbumgrvtx  29932  nbgrnself  29945  uvtxel1  29982  wlkonl1iedg  30249  crctcshwlkn0lem6  30409  2wlkdlem10  30529  1wlkdlem4  30736  3wlkdlem6  30771  3wlkdlem10  30775  eupth2lem3lem4  30837  frcond1  30872  frgr1v  30877  nfrgr2v  30878  frgr3vlem1  30879  frgr3vlem2  30880  frgr3v  30881  4cycl2vnunb  30896  n4cyclfrgr  30897  isssp  31331  ubthlem1  31477  shmodi  31997  chsupid  32019  chsscon3  32107  spansncvi  32259  mdslmd1lem3  32934  mdslmd1lem4  32935  mdsymlem5  33014  dmdbr5ati  33029  dmdbr6ati  33030  dmdbr7ati  33031  ssiun2sf  33201  fpwrelmapffslem  33370  prodindf  33475  pwrssmgc  33607  fldgenval  33920  unitprodclb  33990  esplysply  34249  esplyfvaln  34252  esplyind  34253  resssra  34265  constrsscn  34418  constrextdg2lem  34426  constrextdg2  34427  txomap  34512  locfinreflem  34518  tpr2rico  34590  pnfneige0  34629  rrhre  34699  dya2icoseg2  34956  omsfval  34972  eulerpartlemt0  35047  eulerpartgbij  35050  eulerpartlemr  35052  eulerpartlemgs2  35058  eulerpartlemn  35059  eulerpart  35060  bnj517  35561  bnj1014  35637  bnj1015  35638  bnj1123  35662  bnj1125  35668  bnj1450  35726  bnj1452  35728  rankse  35793  elscott  35795  elkarden  35879  cplgredgex  35981  kur14  36067  cvmliftlem15  36149  cvmlift2lem12  36165  cvmlift2lem13  36166  mclsval  36414  mclsax  36420  mclsppslem  36434  prodeq12sdv  37099  cbvsumdavw2  37176  cbvproddavw2  37177  opnrebl  37200  opnrebl2  37201  ivthALT  37215  neibastop2lem  37240  fnemeet1  37246  filnetlem1  37258  filnetlem4  37261  ttcmin  37376  dfttc2g  37386  bj-imdirval3  38198  bj-imdiridlem  38199  rdgssun  38394  lindsadd  38629  ptrecube  38631  poimirlem32  38663  opnmbllem0  38667  mblfinlem1  38668  mblfinlem2  38669  mblfinlem3  38670  ovoliunnfl  38673  ex-ovoliunnfl  38674  voliunnfl  38675  totbndbnd  38816  heibor1lem  38836  heiborlem10  38847  scottexf  39193  scott0f  39194  relcnveq2  39354  cnvref4  39375  dfcnvrefrels2  39633  dfcnvrefrel2  39635  elrelscnveq2  39654  symrefref2  39672  lcv1  40191  lfl1dim  40271  lfl1dim2N  40272  paddasslem17  40986  dihglblem6  42490  dochvalr  42507  dochord3  42522  lpolconN  42637  lcfls1lem  42684  mapdffval  42776  mapdfval  42777  mapdsn2  42792  mapd0  42815  lspindp5  42920  mapdh8ab  42927  primrootscoprbij  43245  aks6d1c2  43273  aks6d1c6lem3  43315  aks6d1c6lem5  43320  aks6d1c7lem1  43323  ismrcd1  43802  nacsfix  43816  setindtr  44124  hbtlem6  44224  oaabsb  44389  tfsconcatrnss  44445  naddwordnexlem4  44496  clcnvlem  44716  iunrelexpmin1  44801  iunrelexpmin2  44805  relexp0a  44809  cotrcltrcl  44818  trclimalb2  44819  cotrclrcl  44835  sbcheg  44872  clsk1indlem1  45138  isotone1  45141  isotone2  45142  ntrclsiso  45160  ntrclsk2  45161  k0004lem1  45240  k0004lem3  45242  mnuop123d  45339  mnuprdlem1  45349  mnuprdlem2  45350  mnuunid  45354  mnurndlem1  45358  modelaxreplem1  46061  modelaxreplem2  46062  modelaxrep  46064  ssdec  46196  iinssd  46239  iinssdf  46247  ssnnf1octb  46302  iooiinicc  46647  iooiinioc  46661  icccncfext  46990  fourierdlem41  47251  meaiininclem  47589  hoidmvlelem3  47700  hoidmvle  47703  opnvonmbllem1  47735  opnvonmbl  47737  iinhoiicclem  47776  smflim  47880  smflimsuplem7  47929  clnbgrval  49013  clnbgrel  49019  sclnbgrel  49038  isubgredg  49057  isubgruhgr  49059  uhgrimisgrgriclem  49121  uhgrimisgrgric  49122  clnbgrgrimlem  49124  clnbgrgrim  49125  isubgr3stgrlem7  49163  uspgrlimlem1  49179  uspgrlimlem2  49180  uspgrlimlem3  49181  uspgrlim  49183  pgnbgreunbgr  49316  uspgrsprf  49337  iinglb  50026  iscnrm3r  50155  iscnrm3l  50158  imassc  50362  setrecseq  50956