Theorem sseq1d 3978

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

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

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 2701

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

This theorem is referenced by:  sseq12d  3980  eqsstrd  3981  ssiun2s  5012  disjxiun  5104  treq  5222  iunopeqop  5481  dfpo2  6269  preddowncl  6305  funimass1  6598  f1imadifssran  6602  feq1  6666  focofo  6785  fvmptss  6980  fvimacnvi  7024  fvimacnvALT  7029  knatar  7332  ovmptss  8072  fnsuppres  8170  frecseq123  8261  csbfrecsg  8263  frrlem1  8265  frrlem3  8267  frrlem4  8268  frrlem13  8277  frrdmcl  8287  fprresex  8289  dfrecs3  8341  oaordi  8510  oaword2  8517  oawordeulem  8518  omword1  8537  oewordri  8556  oeordsuc  8558  nnaordi  8582  nnawordex  8601  naddcllem  8640  naddunif  8657  ereq1  8678  elpm2r  8818  inficl  9376  fipwss  9380  dffi3  9382  hartogslem1  9495  inf3lema  9577  inf3lemd  9580  cantnfle  9624  cantnflem2  9643  ttrclselem1  9678  trcl  9681  tcmin  9694  rankr1ai  9751  rankxplim  9832  scottex  9838  scott0  9839  scottexs  9840  scott0s  9841  karden  9848  cardne  9918  cardaleph  10042  ackbij2  10195  cflim2  10216  cfslb  10219  coftr  10226  fin23lem15  10287  fin23lem32  10297  fin23lem34  10299  fin23lem35  10300  fin23lem36  10301  fin23lem41  10305  isf32lem1  10306  itunitc1  10373  axdc3lem2  10404  ttukeylem1  10462  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem4  10587  fpwwe2  10596  fpwwecbv  10597  fpwwelem  10598  canthwelem  10603  canthwe  10604  pwfseqlem4  10615  wunex2  10691  wuncval2  10700  eltsk2g  10704  tskpwss  10705  inar1  10728  grothpw  10779  grothpwex  10780  axgroth6  10781  grothac  10783  peano5uzti  12624  fsuppmapnn0fiub0  13958  relexpnndm  15007  rtrclreclem4  15027  dfrtrcl2  15028  lo1o1  15498  o1lo1  15503  o1lo12  15504  lo1eq  15534  rlimeq  15535  isercoll  15634  prmreclem4  16890  vdwmc  16949  vdwlem1  16952  vdwlem2  16953  vdwlem12  16963  vdwlem13  16964  ramval  16979  ramz2  16995  ramub1lem1  16997  isacs2  17614  isacs1i  17618  mreacs  17619  acsfn  17620  rescabs  17795  ipole  18493  ipodrsima  18500  isacs5  18507  symgsssg  19397  psgnunilem5  19424  sylow1  19533  efgval2  19654  efgsfo  19669  frgpuplem  19702  gsumzf1o  19842  gsumzoppg  19874  dprdcntz  19940  islbs2  21064  frlmssuvc1  21703  frlmssuvc2  21704  frlmsslsp  21705  ismhp  22027  pptbas  22895  pnfnei  23107  mnfnei  23108  iscnp  23124  iscnp4  23150  cnntr  23162  cnconst2  23170  cnpresti  23175  cnprest  23176  isreg  23219  isnrm  23222  isnrm2  23245  perfcls  23252  isreg2  23264  hauscmplem  23293  1stcfb  23332  1stcelcls  23348  1stccnp  23349  txbas  23454  ptbasfi  23468  xkoopn  23476  xkoccn  23506  txcnp  23507  ptcnplem  23508  txdis  23519  txdis1cn  23522  txtube  23527  txkgen  23539  xkohaus  23540  xkoptsub  23541  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  reghmph  23680  nrmhmph  23681  trfil2  23774  ufileu  23806  elfm  23834  elfm2  23835  elfm3  23837  imaelfm  23838  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fmco  23848  elflim2  23851  flffbas  23882  lmflf  23892  txflf  23893  fclscf  23912  flimfnfcls  23915  cnextcn  23954  symgtgp  23993  ghmcnp  24002  qustgplem  24008  eltsms  24020  ustval  24090  ust0  24107  trust  24117  utoptop  24122  restutop  24125  restutopopn  24126  utopsnneiplem  24135  ucncn  24172  fmucnd  24179  cfilufg  24180  trcfilu  24181  neipcfilu  24183  blssps  24312  blss  24313  ssblex  24316  blin2  24317  metss2  24400  metrest  24412  metcnp3  24428  metustexhalf  24444  metustbl  24454  psmetutop  24455  xrsmopn  24701  recld2  24703  icccmplem1  24711  icccmplem2  24712  icccmp  24714  reconnlem2  24716  lebnumlem3  24862  lebnum  24863  xlebnum  24864  lebnumii  24865  nmhmcn  25020  cfilfval  25164  caubl  25208  caublcls  25209  bcthlem1  25224  bcth  25229  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  voliunlem3  25453  dyadmax  25499  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  ellimc2  25778  limcnlp  25779  ellimc3  25780  limcflf  25782  limciun  25795  cpnord  25837  lhop  25921  xrlimcnp  26878  cvxcl  26895  dchrval  27145  noetalem2  27654  madebdayim  27799  madebdaylemold  27809  madebday  27811  precsexlem8  28116  ausgrumgri  29094  ausgrusgri  29095  nbgrval  29263  nbgrel  29267  nbumgrvtx  29273  nbgrnself  29286  uvtxel1  29323  wlkonl1iedg  29593  crctcshwlkn0lem6  29745  2wlkdlem10  29865  1wlkdlem4  30069  3wlkdlem6  30094  3wlkdlem10  30098  eupth2lem3lem4  30160  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3vlem1  30202  frgr3vlem2  30203  frgr3v  30204  4cycl2vnunb  30219  n4cyclfrgr  30220  isssp  30653  ubthlem1  30799  shmodi  31319  chsupid  31341  chsscon3  31429  spansncvi  31581  mdslmd1lem3  32256  mdslmd1lem4  32257  mdsymlem5  32336  dmdbr5ati  32351  dmdbr6ati  32352  dmdbr7ati  32353  ssiun2sf  32488  fpwrelmapffslem  32655  prodindf  32786  pwrssmgc  32926  fldgenval  33262  unitprodclb  33360  resssra  33583  constrsscn  33730  constrextdg2lem  33738  constrextdg2  33739  txomap  33824  locfinreflem  33830  tpr2rico  33902  pnfneige0  33941  rrhre  34011  dya2icoseg2  34269  omsfval  34285  eulerpartlemt0  34360  eulerpartgbij  34363  eulerpartlemr  34365  eulerpartlemgs2  34371  eulerpartlemn  34372  eulerpart  34373  bnj517  34875  bnj1014  34951  bnj1015  34952  bnj1123  34976  bnj1125  34982  bnj1450  35040  bnj1452  35042  cplgredgex  35108  kur14  35203  cvmliftlem15  35285  cvmlift2lem12  35301  cvmlift2lem13  35302  mclsval  35550  mclsax  35556  mclsppslem  35570  prodeq12sdv  36206  cbvsumdavw2  36283  cbvproddavw2  36284  opnrebl  36308  opnrebl2  36309  ivthALT  36323  neibastop2lem  36348  fnemeet1  36354  filnetlem1  36366  filnetlem4  36369  bj-imdirval3  37172  bj-imdiridlem  37173  rdgssun  37366  lindsadd  37607  lindsenlbs  37609  ptrecube  37614  poimirlem32  37646  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  ovoliunnfl  37656  ex-ovoliunnfl  37657  voliunnfl  37658  totbndbnd  37783  heibor1lem  37803  heiborlem10  37814  scottexf  38162  scott0f  38163  relcnveq2  38311  cnvref4  38332  elrelscnveq2  38484  dfcnvrefrels2  38519  dfcnvrefrel2  38521  symrefref2  38554  lcv1  39034  lfl1dim  39114  lfl1dim2N  39115  paddasslem17  39830  dihglblem6  41334  dochvalr  41351  dochord3  41366  lpolconN  41481  lcfls1lem  41528  mapdffval  41620  mapdfval  41621  mapdsn2  41636  mapd0  41659  lspindp5  41764  mapdh8ab  41771  primrootscoprbij  42090  aks6d1c2  42118  aks6d1c6lem3  42160  aks6d1c6lem5  42165  aks6d1c7lem1  42168  ismrcd1  42686  nacsfix  42700  setindtr  43013  hbtlem6  43118  oaabsb  43283  tfsconcatrnss  43339  naddwordnexlem4  43390  clcnvlem  43612  iunrelexpmin1  43697  iunrelexpmin2  43701  relexp0a  43705  cotrcltrcl  43714  trclimalb2  43715  cotrclrcl  43731  sbcheg  43768  clsk1indlem1  44034  isotone1  44037  isotone2  44038  ntrclsiso  44056  ntrclsk2  44057  k0004lem1  44136  k0004lem3  44138  scottelrankd  44236  mnuop123d  44251  mnuprdlem1  44261  mnuprdlem2  44262  mnuunid  44266  mnurndlem1  44270  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  ssdec  45082  iinssd  45125  iinssdf  45133  ssnnf1octb  45188  iooiinicc  45540  iooiinioc  45554  icccncfext  45885  fourierdlem41  46146  meaiininclem  46484  hoidmvlelem3  46595  hoidmvle  46598  opnvonmbllem1  46630  opnvonmbl  46632  iinhoiicclem  46671  smflim  46775  smflimsuplem7  46824  clnbgrval  47823  clnbgrel  47829  sclnbgrel  47847  isubgredg  47866  isubgruhgr  47868  uhgrimisgrgriclem  47930  uhgrimisgrgric  47931  clnbgrgrimlem  47933  clnbgrgrim  47934  isubgr3stgrlem7  47971  uspgrlimlem1  47987  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlim  47991  pgnbgreunbgr  48115  uspgrsprf  48134  iinglb  48810  iscnrm3r  48936  iscnrm3l  48939  imassc  49142  setrecseq  49674  setrec1lem4  49679  setrec2fun  49681