Theorem sseq1d 3953

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  sseq12d  3955  eqsstrd  3956  ssiun2s  4991  disjxiun  5082  treq  5199  iunopeqop  5475  iunopeqopOLD  5476  dfpo2  6260  preddowncl  6296  funimass1  6580  f1imadifssran  6584  feq1  6646  focofo  6765  fvmptss  6960  fvimacnvi  7004  fvimacnvALT  7009  knatar  7312  ovmptss  8043  fnsuppres  8141  frecseq123  8232  csbfrecsg  8234  frrlem1  8236  frrlem3  8238  frrlem4  8239  frrlem13  8248  frrdmcl  8258  fprresex  8260  dfrecs3  8312  oaordi  8481  oaword2  8488  oawordeulem  8489  omword1  8508  oewordri  8528  oeordsuc  8530  nnaordi  8554  nnawordex  8573  naddcllem  8612  naddunif  8629  ereq1  8651  elpm2r  8792  inficl  9338  fipwss  9342  dffi3  9344  hartogslem1  9457  inf3lema  9545  inf3lemd  9548  cantnfle  9592  cantnflem2  9611  ttrclselem1  9646  trcl  9649  tcmin  9660  rankr1ai  9722  rankxplim  9803  scottex  9809  scott0  9810  scottexs  9811  scott0s  9812  karden  9819  cardne  9889  cardaleph  10011  ackbij2  10164  cflim2  10185  cfslb  10188  coftr  10195  fin23lem15  10256  fin23lem32  10266  fin23lem34  10268  fin23lem35  10269  fin23lem36  10270  fin23lem41  10274  isf32lem1  10275  itunitc1  10342  axdc3lem2  10373  ttukeylem1  10431  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwe2  10566  fpwwecbv  10567  fpwwelem  10568  canthwelem  10573  canthwe  10574  pwfseqlem4  10585  wunex2  10661  wuncval2  10670  eltsk2g  10674  tskpwss  10675  inar1  10698  grothpw  10749  grothpwex  10750  axgroth6  10751  grothac  10753  peano5uzti  12619  fsuppmapnn0fiub0  13955  relexpnndm  15003  rtrclreclem4  15023  dfrtrcl2  15024  lo1o1  15494  o1lo1  15499  o1lo12  15500  lo1eq  15530  rlimeq  15531  isercoll  15630  prmreclem4  16890  vdwmc  16949  vdwlem1  16952  vdwlem2  16953  vdwlem12  16963  vdwlem13  16964  ramval  16979  ramz2  16995  ramub1lem1  16997  isacs2  17619  isacs1i  17623  mreacs  17624  acsfn  17625  rescabs  17800  ipole  18500  ipodrsima  18507  isacs5  18514  symgsssg  19442  psgnunilem5  19469  sylow1  19578  efgval2  19699  efgsfo  19714  frgpuplem  19747  gsumzf1o  19887  gsumzoppg  19919  dprdcntz  19985  islbs2  21152  frlmssuvc1  21774  frlmssuvc2  21775  frlmsslsp  21776  ismhp  22106  pptbas  22973  pnfnei  23185  mnfnei  23186  iscnp  23202  iscnp4  23228  cnntr  23240  cnconst2  23248  cnpresti  23253  cnprest  23254  isreg  23297  isnrm  23300  isnrm2  23323  perfcls  23330  isreg2  23342  hauscmplem  23371  1stcfb  23410  1stcelcls  23426  1stccnp  23427  txbas  23532  ptbasfi  23546  xkoopn  23554  xkoccn  23584  txcnp  23585  ptcnplem  23586  txdis  23597  txdis1cn  23600  txtube  23605  txkgen  23617  xkohaus  23618  xkoptsub  23619  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  xkococn  23625  xkoinjcn  23652  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  reghmph  23758  nrmhmph  23759  trfil2  23852  ufileu  23884  elfm  23912  elfm2  23913  elfm3  23915  imaelfm  23916  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fmco  23926  elflim2  23929  flffbas  23960  lmflf  23970  txflf  23971  fclscf  23990  flimfnfcls  23993  cnextcn  24032  symgtgp  24071  ghmcnp  24080  qustgplem  24086  eltsms  24098  ustval  24168  ust0  24185  trust  24194  utoptop  24199  restutop  24202  restutopopn  24203  utopsnneiplem  24212  ucncn  24249  fmucnd  24256  cfilufg  24257  trcfilu  24258  neipcfilu  24260  blssps  24389  blss  24390  ssblex  24393  blin2  24394  metss2  24477  metrest  24489  metcnp3  24505  metustexhalf  24521  metustbl  24531  psmetutop  24532  xrsmopn  24778  recld2  24780  icccmplem1  24788  icccmplem2  24789  icccmp  24791  reconnlem2  24793  lebnumlem3  24930  lebnum  24931  xlebnum  24932  lebnumii  24933  nmhmcn  25087  cfilfval  25231  caubl  25275  caublcls  25276  bcthlem1  25291  bcth  25296  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  ovoliunnul  25474  voliunlem3  25519  dyadmax  25565  dyadmbllem  25566  dyadmbl  25567  opnmbllem  25568  ellimc2  25844  limcnlp  25845  ellimc3  25846  limcflf  25848  limciun  25861  cpnord  25902  lhop  25983  xrlimcnp  26932  cvxcl  26948  dchrval  27197  noetalem2  27706  madebdayim  27880  madebdaylemold  27890  madebday  27892  bdayle  27908  precsexlem8  28206  bdaypw2n0bndlem  28455  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  bdayfinbnd  28461  ausgrumgri  29236  ausgrusgri  29237  nbgrval  29405  nbgrel  29409  nbumgrvtx  29415  nbgrnself  29428  uvtxel1  29465  wlkonl1iedg  29732  crctcshwlkn0lem6  29883  2wlkdlem10  30003  1wlkdlem4  30210  3wlkdlem6  30235  3wlkdlem10  30239  eupth2lem3lem4  30301  frcond1  30336  frgr1v  30341  nfrgr2v  30342  frgr3vlem1  30343  frgr3vlem2  30344  frgr3v  30345  4cycl2vnunb  30360  n4cyclfrgr  30361  isssp  30795  ubthlem1  30941  shmodi  31461  chsupid  31483  chsscon3  31571  spansncvi  31723  mdslmd1lem3  32398  mdslmd1lem4  32399  mdsymlem5  32478  dmdbr5ati  32493  dmdbr6ati  32494  dmdbr7ati  32495  ssiun2sf  32629  fpwrelmapffslem  32805  prodindf  32922  pwrssmgc  33060  fldgenval  33373  unitprodclb  33449  esplysply  33715  esplyfvaln  33718  esplyind  33719  resssra  33731  constrsscn  33884  constrextdg2lem  33892  constrextdg2  33893  txomap  33978  locfinreflem  33984  tpr2rico  34056  pnfneige0  34095  rrhre  34165  dya2icoseg2  34422  omsfval  34438  eulerpartlemt0  34513  eulerpartgbij  34516  eulerpartlemr  34518  eulerpartlemgs2  34524  eulerpartlemn  34525  eulerpart  34526  bnj517  35027  bnj1014  35103  bnj1015  35104  bnj1123  35128  bnj1125  35134  bnj1450  35192  bnj1452  35194  cplgredgex  35303  kur14  35398  cvmliftlem15  35480  cvmlift2lem12  35496  cvmlift2lem13  35497  mclsval  35745  mclsax  35751  mclsppslem  35765  prodeq12sdv  36400  cbvsumdavw2  36477  cbvproddavw2  36478  opnrebl  36502  opnrebl2  36503  ivthALT  36517  neibastop2lem  36542  fnemeet1  36548  filnetlem1  36560  filnetlem4  36563  ttcmin  36678  dfttc2g  36688  bj-imdirval3  37498  bj-imdiridlem  37499  rdgssun  37694  lindsadd  37934  lindsenlbs  37936  ptrecube  37941  poimirlem32  37973  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  ovoliunnfl  37983  ex-ovoliunnfl  37984  voliunnfl  37985  totbndbnd  38110  heibor1lem  38130  heiborlem10  38141  scottexf  38489  scott0f  38490  relcnveq2  38650  cnvref4  38671  dfcnvrefrels2  38929  dfcnvrefrel2  38931  elrelscnveq2  38950  symrefref2  38968  lcv1  39487  lfl1dim  39567  lfl1dim2N  39568  paddasslem17  40282  dihglblem6  41786  dochvalr  41803  dochord3  41818  lpolconN  41933  lcfls1lem  41980  mapdffval  42072  mapdfval  42073  mapdsn2  42088  mapd0  42111  lspindp5  42216  mapdh8ab  42223  primrootscoprbij  42541  aks6d1c2  42569  aks6d1c6lem3  42611  aks6d1c6lem5  42616  aks6d1c7lem1  42619  ismrcd1  43130  nacsfix  43144  setindtr  43452  hbtlem6  43557  oaabsb  43722  tfsconcatrnss  43778  naddwordnexlem4  43829  clcnvlem  44050  iunrelexpmin1  44135  iunrelexpmin2  44139  relexp0a  44143  cotrcltrcl  44152  trclimalb2  44153  cotrclrcl  44169  sbcheg  44206  clsk1indlem1  44472  isotone1  44475  isotone2  44476  ntrclsiso  44494  ntrclsk2  44495  k0004lem1  44574  k0004lem3  44576  scottelrankd  44674  mnuop123d  44689  mnuprdlem1  44699  mnuprdlem2  44700  mnuunid  44704  mnurndlem1  44708  modelaxreplem1  45405  modelaxreplem2  45406  modelaxrep  45408  ssdec  45518  iinssd  45561  iinssdf  45569  ssnnf1octb  45624  iooiinicc  45972  iooiinioc  45986  icccncfext  46315  fourierdlem41  46576  meaiininclem  46914  hoidmvlelem3  47025  hoidmvle  47028  opnvonmbllem1  47060  opnvonmbl  47062  iinhoiicclem  47101  smflim  47205  smflimsuplem7  47254  clnbgrval  48298  clnbgrel  48304  sclnbgrel  48323  isubgredg  48342  isubgruhgr  48344  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrimlem  48409  clnbgrgrim  48410  isubgr3stgrlem7  48448  uspgrlimlem1  48464  uspgrlimlem2  48465  uspgrlimlem3  48466  uspgrlim  48468  pgnbgreunbgr  48601  uspgrsprf  48622  iinglb  49297  iscnrm3r  49423  iscnrm3l  49426  imassc  49628  setrecseq  50160  setrec1lem4  50165  setrec2fun  50167