Theorem sseq1d 3965

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

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

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 2734

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

This theorem is used by:  sseq12d  3967  eqsstrd  3968  ssiun2s  5011  disjxiun  5104  treq  5223  iunopeqop  5502  iunopeqopOLD  5503  dfpo2  6298  preddowncl  6334  funimass1  6619  feq1  6684  focofo  6806  fvmptss  7003  fvimacnvi  7048  fvimacnvALT  7053  knatar  7364  ovmptss  8094  fnsuppres  8193  frecseq123  8285  csbfrecsg  8287  frrlem1  8289  frrlem3  8291  frrlem4  8292  frrlem13  8301  frrdmcl  8311  fprresex  8313  dfrecs3  8365  oaordi  8537  oaword2  8544  oawordeulem  8545  omword1  8564  oewordri  8584  oeordsuc  8586  nnaordi  8610  nnawordex  8629  naddcllem  8668  naddunif  8686  ereq1  8708  elpm2r  8848  inficl  9399  fipwss  9403  dffi3  9405  hartogslem1  9518  inf3lema  9607  inf3lemd  9610  cantnfle  9654  cantnflem2  9673  ttrclselem1  9708  trcl  9711  tcmin  9722  rankr1ai  9784  rankxplim  9865  scottex  9876  scottexOLD  9877  scott0b  9880  scott0OLD  9881  scottexsOLD  9886  scott0bsOLD  9888  scottelrankd  9891  kardenOLD  9903  cardne  9974  cardaleph  10096  ackbij2  10248  cflim2  10269  cfslb  10272  coftr  10279  fin23lem15  10340  fin23lem32  10350  fin23lem34  10352  fin23lem35  10353  fin23lem36  10354  fin23lem41  10358  isf32lem1  10359  itunitc1  10426  axdc3lem2  10457  ttukeylem1  10515  fpwwe2cbv  10643  fpwwe2lem2  10645  fpwwe2lem4  10647  fpwwe2  10656  fpwwecbv  10657  fpwwelem  10658  canthwelem  10663  canthwe  10664  pwfseqlem4  10675  wunex2  10751  wuncval2  10760  eltsk2g  10764  tskpwss  10765  inar1  10788  grothpw  10839  grothpwex  10840  axgroth6  10841  grothac  10843  peano5uzti  12715  fsuppmapnn0fiub0  14061  relexpnndm  15118  rtrclreclem4  15138  dfrtrcl2  15139  lo1o1  15623  o1lo1  15628  o1lo12  15629  lo1eq  15659  rlimeq  15660  isercoll  15759  prmreclem4  17017  vdwmc  17076  vdwlem1  17079  vdwlem2  17080  vdwlem12  17090  vdwlem13  17091  ramval  17106  ramz2  17122  ramub1lem1  17124  isacs2  17747  isacs1i  17751  mreacs  17752  acsfn  17753  rescabs  17928  ipole  18628  ipodrsima  18635  isacs5  18642  symgsssg  19600  psgnunilem5  19627  sylow1  19736  efgval2  19857  efgsfo  19872  frgpuplem  19905  gsumzf1o  20045  gsumzoppg  20077  dprdcntz  20143  islbs2  21347  frlmssuvc1  22013  frlmssuvc2  22014  frlmsslsp  22015  lindsenlbs  22070  ismhp  22374  pptbas  23239  pnfnei  23451  mnfnei  23452  iscnp  23468  iscnp4  23494  cnntr  23506  cnconst2  23514  cnpresti  23519  cnprest  23520  isreg  23563  isnrm  23566  isnrm2  23589  perfcls  23596  isreg2  23608  hauscmplem  23637  1stcfb  23676  1stcelcls  23693  1stccnp  23694  txbas  23799  ptbasfi  23813  xkoopn  23821  xkoccn  23851  txcnp  23852  ptcnplem  23853  txdis  23864  txdis1cn  23867  txtube  23872  txkgen  23884  xkohaus  23885  xkoptsub  23886  xkoco1cn  23889  xkoco2cn  23890  xkococnlem  23891  xkococn  23892  xkoinjcn  23919  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  reghmph  24025  nrmhmph  24026  trfil2  24119  ufileu  24151  elfm  24179  elfm2  24180  elfm3  24182  imaelfm  24183  rnelfm  24185  fmfnfmlem2  24187  fmfnfmlem4  24189  fmco  24193  elflim2  24196  flffbas  24227  lmflf  24237  txflf  24238  fclscf  24257  flimfnfcls  24260  cnextcn  24299  symgtgp  24338  ghmcnp  24347  qustgplem  24353  eltsms  24365  ustval  24435  ust0  24452  trust  24461  utoptop  24466  restutop  24469  restutopopn  24470  utopsnneiplem  24479  ucncn  24516  fmucnd  24523  cfilufg  24524  trcfilu  24525  neipcfilu  24527  blssps  24656  blss  24657  ssblex  24660  blin2  24661  metss2  24744  metrest  24756  metcnp3  24772  metustexhalf  24788  metustbl  24798  psmetutop  24799  xrsmopn  25045  recld2  25047  icccmplem1  25055  icccmplem2  25056  icccmp  25058  reconnlem2  25060  lebnumlem3  25197  lebnum  25198  xlebnum  25199  lebnumii  25200  nmhmcn  25354  cfilfval  25498  caubl  25542  caublcls  25543  bcthlem1  25558  bcth  25563  ovolfiniun  25735  ovoliunlem3  25738  ovoliun  25739  ovoliun2  25740  ovoliunnul  25741  voliunlem3  25786  dyadmax  25832  dyadmbllem  25833  dyadmbl  25834  opnmbllem  25835  ellimc2  26111  limcnlp  26112  ellimc3  26113  limcflf  26115  limciun  26128  cpnord  26169  lhop  26250  xrlimcnp  27213  cvxcl  27229  dchrval  27478  noetalem2  27986  madebdayim  28161  madebdaylemold  28171  madebday  28173  bdayle  28189  precsexlem8  28487  bdaypw2n0bndlem  28736  bdayfinbndcbv  28739  bdayfinbndlem1  28740  bdayfinbndlem2  28741  bdayfinbnd  28742  lnssplng  29157  ausgrumgri  29635  ausgrusgri  29636  nbgrval  29804  nbgrel  29808  nbumgrvtx  29814  nbgrnself  29827  uvtxel1  29864  wlkonl1iedg  30131  crctcshwlkn0lem6  30291  2wlkdlem10  30411  1wlkdlem4  30618  3wlkdlem6  30653  3wlkdlem10  30657  eupth2lem3lem4  30719  frcond1  30754  frgr1v  30759  nfrgr2v  30760  frgr3vlem1  30761  frgr3vlem2  30762  frgr3v  30763  4cycl2vnunb  30778  n4cyclfrgr  30779  isssp  31213  ubthlem1  31359  shmodi  31879  chsupid  31901  chsscon3  31989  spansncvi  32141  mdslmd1lem3  32816  mdslmd1lem4  32817  mdsymlem5  32896  dmdbr5ati  32911  dmdbr6ati  32912  dmdbr7ati  32913  ssiun2sf  33041  fpwrelmapffslem  33211  prodindf  33316  pwrssmgc  33448  fldgenval  33761  unitprodclb  33830  esplysply  34089  esplyfvaln  34092  esplyind  34093  resssra  34105  constrsscn  34258  constrextdg2lem  34266  constrextdg2  34267  txomap  34352  locfinreflem  34358  tpr2rico  34430  pnfneige0  34469  rrhre  34539  dya2icoseg2  34797  omsfval  34813  eulerpartlemt0  34888  eulerpartgbij  34891  eulerpartlemr  34893  eulerpartlemgs2  34899  eulerpartlemn  34900  eulerpart  34901  bnj517  35402  bnj1014  35478  bnj1015  35479  bnj1123  35503  bnj1125  35509  bnj1450  35567  bnj1452  35569  elscott  35632  elkarden  35689  cplgredgex  35727  kur14  35803  cvmliftlem15  35885  cvmlift2lem12  35901  cvmlift2lem13  35902  mclsval  36150  mclsax  36156  mclsppslem  36170  prodeq12sdv  36846  cbvsumdavw2  36923  cbvproddavw2  36924  opnrebl  36947  opnrebl2  36948  ivthALT  36962  neibastop2lem  36987  fnemeet1  36993  filnetlem1  37005  filnetlem4  37008  ttcmin  37123  dfttc2g  37133  bj-imdirval3  37944  bj-imdiridlem  37945  rdgssun  38140  lindsadd  38375  ptrecube  38377  poimirlem32  38409  opnmbllem0  38413  mblfinlem1  38414  mblfinlem2  38415  mblfinlem3  38416  ovoliunnfl  38419  ex-ovoliunnfl  38420  voliunnfl  38421  totbndbnd  38547  heibor1lem  38567  heiborlem10  38578  scottexf  38924  scott0f  38925  relcnveq2  39085  cnvref4  39106  dfcnvrefrels2  39364  dfcnvrefrel2  39366  elrelscnveq2  39385  symrefref2  39403  lcv1  39922  lfl1dim  40002  lfl1dim2N  40003  paddasslem17  40717  dihglblem6  42221  dochvalr  42238  dochord3  42253  lpolconN  42368  lcfls1lem  42415  mapdffval  42507  mapdfval  42508  mapdsn2  42523  mapd0  42546  lspindp5  42651  mapdh8ab  42658  primrootscoprbij  42976  aks6d1c2  43004  aks6d1c6lem3  43046  aks6d1c6lem5  43051  aks6d1c7lem1  43054  ismrcd1  43551  nacsfix  43565  setindtr  43873  hbtlem6  43978  oaabsb  44143  tfsconcatrnss  44199  naddwordnexlem4  44250  clcnvlem  44471  iunrelexpmin1  44556  iunrelexpmin2  44560  relexp0a  44564  cotrcltrcl  44573  trclimalb2  44574  cotrclrcl  44590  sbcheg  44627  clsk1indlem1  44893  isotone1  44896  isotone2  44897  ntrclsiso  44915  ntrclsk2  44916  k0004lem1  44995  k0004lem3  44997  mnuop123d  45094  mnuprdlem1  45104  mnuprdlem2  45105  mnuunid  45109  mnurndlem1  45113  modelaxreplem1  45809  modelaxreplem2  45810  modelaxrep  45812  ssdec  45928  iinssd  45971  iinssdf  45979  ssnnf1octb  46034  iooiinicc  46380  iooiinioc  46394  icccncfext  46723  fourierdlem41  46984  meaiininclem  47322  hoidmvlelem3  47433  hoidmvle  47436  opnvonmbllem1  47468  opnvonmbl  47470  iinhoiicclem  47509  smflim  47613  smflimsuplem7  47662  clnbgrval  48746  clnbgrel  48752  sclnbgrel  48771  isubgredg  48790  isubgruhgr  48792  uhgrimisgrgriclem  48854  uhgrimisgrgric  48855  clnbgrgrimlem  48857  clnbgrgrim  48858  isubgr3stgrlem7  48896  uspgrlimlem1  48912  uspgrlimlem2  48913  uspgrlimlem3  48914  uspgrlim  48916  pgnbgreunbgr  49049  uspgrsprf  49070  iinglb  49758  iscnrm3r  49882  iscnrm3l  49885  imassc  50087  setrecseq  50619  setrec1lem4  50624  setrec2fun  50626