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 17	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseq12d  3964  eqsstrd  3965  ssiun2s  4999  disjxiun  5090  treq  5207  iunopeqop  5464  dfpo2  6248  preddowncl  6284  funimass1  6568  f1imadifssran  6572  feq1  6634  focofo  6753  fvmptss  6947  fvimacnvi  6991  fvimacnvALT  6996  knatar  7297  ovmptss  8029  fnsuppres  8127  frecseq123  8218  csbfrecsg  8220  frrlem1  8222  frrlem3  8224  frrlem4  8225  frrlem13  8234  frrdmcl  8244  fprresex  8246  dfrecs3  8298  oaordi  8467  oaword2  8474  oawordeulem  8475  omword1  8494  oewordri  8513  oeordsuc  8515  nnaordi  8539  nnawordex  8558  naddcllem  8597  naddunif  8614  ereq1  8635  elpm2r  8775  inficl  9316  fipwss  9320  dffi3  9322  hartogslem1  9435  inf3lema  9521  inf3lemd  9524  cantnfle  9568  cantnflem2  9587  ttrclselem1  9622  trcl  9625  tcmin  9636  rankr1ai  9698  rankxplim  9779  scottex  9785  scott0  9786  scottexs  9787  scott0s  9788  karden  9795  cardne  9865  cardaleph  9987  ackbij2  10140  cflim2  10161  cfslb  10164  coftr  10171  fin23lem15  10232  fin23lem32  10242  fin23lem34  10244  fin23lem35  10245  fin23lem36  10246  fin23lem41  10250  isf32lem1  10251  itunitc1  10318  axdc3lem2  10349  ttukeylem1  10407  fpwwe2cbv  10528  fpwwe2lem2  10530  fpwwe2lem4  10532  fpwwe2  10541  fpwwecbv  10542  fpwwelem  10543  canthwelem  10548  canthwe  10549  pwfseqlem4  10560  wunex2  10636  wuncval2  10645  eltsk2g  10649  tskpwss  10650  inar1  10673  grothpw  10724  grothpwex  10725  axgroth6  10726  grothac  10728  peano5uzti  12569  fsuppmapnn0fiub0  13902  relexpnndm  14950  rtrclreclem4  14970  dfrtrcl2  14971  lo1o1  15441  o1lo1  15446  o1lo12  15447  lo1eq  15477  rlimeq  15478  isercoll  15577  prmreclem4  16833  vdwmc  16892  vdwlem1  16895  vdwlem2  16896  vdwlem12  16906  vdwlem13  16907  ramval  16922  ramz2  16938  ramub1lem1  16940  isacs2  17561  isacs1i  17565  mreacs  17566  acsfn  17567  rescabs  17742  ipole  18442  ipodrsima  18449  isacs5  18456  symgsssg  19381  psgnunilem5  19408  sylow1  19517  efgval2  19638  efgsfo  19653  frgpuplem  19686  gsumzf1o  19826  gsumzoppg  19858  dprdcntz  19924  islbs2  21093  frlmssuvc1  21733  frlmssuvc2  21734  frlmsslsp  21735  ismhp  22056  pptbas  22924  pnfnei  23136  mnfnei  23137  iscnp  23153  iscnp4  23179  cnntr  23191  cnconst2  23199  cnpresti  23204  cnprest  23205  isreg  23248  isnrm  23251  isnrm2  23274  perfcls  23281  isreg2  23293  hauscmplem  23322  1stcfb  23361  1stcelcls  23377  1stccnp  23378  txbas  23483  ptbasfi  23497  xkoopn  23505  xkoccn  23535  txcnp  23536  ptcnplem  23537  txdis  23548  txdis1cn  23551  txtube  23556  txkgen  23568  xkohaus  23569  xkoptsub  23570  xkoco1cn  23573  xkoco2cn  23574  xkococnlem  23575  xkococn  23576  xkoinjcn  23603  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  reghmph  23709  nrmhmph  23710  trfil2  23803  ufileu  23835  elfm  23863  elfm2  23864  elfm3  23866  imaelfm  23867  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  fmco  23877  elflim2  23880  flffbas  23911  lmflf  23921  txflf  23922  fclscf  23941  flimfnfcls  23944  cnextcn  23983  symgtgp  24022  ghmcnp  24031  qustgplem  24037  eltsms  24049  ustval  24119  ust0  24136  trust  24145  utoptop  24150  restutop  24153  restutopopn  24154  utopsnneiplem  24163  ucncn  24200  fmucnd  24207  cfilufg  24208  trcfilu  24209  neipcfilu  24211  blssps  24340  blss  24341  ssblex  24344  blin2  24345  metss2  24428  metrest  24440  metcnp3  24456  metustexhalf  24472  metustbl  24482  psmetutop  24483  xrsmopn  24729  recld2  24731  icccmplem1  24739  icccmplem2  24740  icccmp  24742  reconnlem2  24744  lebnumlem3  24890  lebnum  24891  xlebnum  24892  lebnumii  24893  nmhmcn  25048  cfilfval  25192  caubl  25236  caublcls  25237  bcthlem1  25252  bcth  25257  ovolfiniun  25430  ovoliunlem3  25433  ovoliun  25434  ovoliun2  25435  ovoliunnul  25436  voliunlem3  25481  dyadmax  25527  dyadmbllem  25528  dyadmbl  25529  opnmbllem  25530  ellimc2  25806  limcnlp  25807  ellimc3  25808  limcflf  25810  limciun  25823  cpnord  25865  lhop  25949  xrlimcnp  26906  cvxcl  26923  dchrval  27173  noetalem2  27682  madebdayim  27834  madebdaylemold  27844  madebday  27846  bdayle  27862  precsexlem8  28153  ausgrumgri  29147  ausgrusgri  29148  nbgrval  29316  nbgrel  29320  nbumgrvtx  29326  nbgrnself  29339  uvtxel1  29376  wlkonl1iedg  29644  crctcshwlkn0lem6  29795  2wlkdlem10  29915  1wlkdlem4  30122  3wlkdlem6  30147  3wlkdlem10  30151  eupth2lem3lem4  30213  frcond1  30248  frgr1v  30253  nfrgr2v  30254  frgr3vlem1  30255  frgr3vlem2  30256  frgr3v  30257  4cycl2vnunb  30272  n4cyclfrgr  30273  isssp  30706  ubthlem1  30852  shmodi  31372  chsupid  31394  chsscon3  31482  spansncvi  31634  mdslmd1lem3  32309  mdslmd1lem4  32310  mdsymlem5  32389  dmdbr5ati  32404  dmdbr6ati  32405  dmdbr7ati  32406  ssiun2sf  32541  fpwrelmapffslem  32719  prodindf  32851  pwrssmgc  32988  fldgenval  33285  unitprodclb  33361  esplysply  33611  esplyind  33613  resssra  33620  constrsscn  33774  constrextdg2lem  33782  constrextdg2  33783  txomap  33868  locfinreflem  33874  tpr2rico  33946  pnfneige0  33985  rrhre  34055  dya2icoseg2  34312  omsfval  34328  eulerpartlemt0  34403  eulerpartgbij  34406  eulerpartlemr  34408  eulerpartlemgs2  34414  eulerpartlemn  34415  eulerpart  34416  bnj517  34918  bnj1014  34994  bnj1015  34995  bnj1123  35019  bnj1125  35025  bnj1450  35083  bnj1452  35085  cplgredgex  35186  kur14  35281  cvmliftlem15  35363  cvmlift2lem12  35379  cvmlift2lem13  35380  mclsval  35628  mclsax  35634  mclsppslem  35648  prodeq12sdv  36283  cbvsumdavw2  36360  cbvproddavw2  36361  opnrebl  36385  opnrebl2  36386  ivthALT  36400  neibastop2lem  36425  fnemeet1  36431  filnetlem1  36443  filnetlem4  36446  bj-imdirval3  37249  bj-imdiridlem  37250  rdgssun  37443  lindsadd  37673  lindsenlbs  37675  ptrecube  37680  poimirlem32  37712  opnmbllem0  37716  mblfinlem1  37717  mblfinlem2  37718  mblfinlem3  37719  ovoliunnfl  37722  ex-ovoliunnfl  37723  voliunnfl  37724  totbndbnd  37849  heibor1lem  37869  heiborlem10  37880  scottexf  38228  scott0f  38229  relcnveq2  38381  cnvref4  38402  dfcnvrefrels2  38640  dfcnvrefrel2  38642  elrelscnveq2  38661  symrefref2  38679  lcv1  39160  lfl1dim  39240  lfl1dim2N  39241  paddasslem17  39955  dihglblem6  41459  dochvalr  41476  dochord3  41491  lpolconN  41606  lcfls1lem  41653  mapdffval  41745  mapdfval  41746  mapdsn2  41761  mapd0  41784  lspindp5  41889  mapdh8ab  41896  primrootscoprbij  42215  aks6d1c2  42243  aks6d1c6lem3  42285  aks6d1c6lem5  42290  aks6d1c7lem1  42293  ismrcd1  42815  nacsfix  42829  setindtr  43141  hbtlem6  43246  oaabsb  43411  tfsconcatrnss  43467  naddwordnexlem4  43518  clcnvlem  43740  iunrelexpmin1  43825  iunrelexpmin2  43829  relexp0a  43833  cotrcltrcl  43842  trclimalb2  43843  cotrclrcl  43859  sbcheg  43896  clsk1indlem1  44162  isotone1  44165  isotone2  44166  ntrclsiso  44184  ntrclsk2  44185  k0004lem1  44264  k0004lem3  44266  scottelrankd  44364  mnuop123d  44379  mnuprdlem1  44389  mnuprdlem2  44390  mnuunid  44394  mnurndlem1  44398  modelaxreplem1  45095  modelaxreplem2  45096  modelaxrep  45098  ssdec  45209  iinssd  45252  iinssdf  45260  ssnnf1octb  45315  iooiinicc  45666  iooiinioc  45680  icccncfext  46009  fourierdlem41  46270  meaiininclem  46608  hoidmvlelem3  46719  hoidmvle  46722  opnvonmbllem1  46754  opnvonmbl  46756  iinhoiicclem  46795  smflim  46899  smflimsuplem7  46948  clnbgrval  47946  clnbgrel  47952  sclnbgrel  47971  isubgredg  47990  isubgruhgr  47992  uhgrimisgrgriclem  48054  uhgrimisgrgric  48055  clnbgrgrimlem  48057  clnbgrgrim  48058  isubgr3stgrlem7  48096  uspgrlimlem1  48112  uspgrlimlem2  48113  uspgrlimlem3  48114  uspgrlim  48116  pgnbgreunbgr  48249  uspgrsprf  48270  iinglb  48946  iscnrm3r  49072  iscnrm3l  49075  imassc  49278  setrecseq  49810  setrec1lem4  49815  setrec2fun  49817