Theorem sseq1d 3975

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ⊆ wss 3910

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927

This theorem is referenced by:  sseq12d  3977  eqsstrd  3982  ssiun2s  5008  disjxiun  5102  treq  5230  iunopeqop  5478  dfpo2  6248  preddowncl  6286  funimass1  6583  feq1  6649  focofo  6769  fvmptss  6960  fvimacnvi  7002  fvimacnvALT  7007  knatar  7302  ovmptss  8025  fnsuppres  8122  frecseq123  8213  csbfrecsg  8215  frrlem1  8217  frrlem3  8219  frrlem4  8220  frrlem13  8229  frrdmcl  8239  fprresex  8241  wrecseq123OLD  8246  wfrlem1OLD  8254  wfrlem3OLD  8256  wfrdmclOLD  8263  wfrlem15OLD  8269  wfrlem17OLD  8271  dfrecs3  8318  dfrecs3OLD  8319  oaordi  8493  oaword2  8500  oawordeulem  8501  omword1  8520  oewordri  8539  oeordsuc  8541  nnaordi  8565  nnawordex  8584  naddcllem  8622  naddunif  8637  ereq1  8655  elpm2r  8783  inficl  9361  fipwss  9365  dffi3  9367  hartogslem1  9478  inf3lema  9560  inf3lemd  9563  cantnfle  9607  cantnflem2  9626  ttrclselem1  9661  trcl  9664  tcmin  9677  rankr1ai  9734  rankxplim  9815  scottex  9821  scott0  9822  scottexs  9823  scott0s  9824  karden  9831  cardne  9901  cardaleph  10025  ackbij2  10179  cflim2  10199  cfslb  10202  coftr  10209  fin23lem15  10270  fin23lem32  10280  fin23lem34  10282  fin23lem35  10283  fin23lem36  10284  fin23lem41  10288  isf32lem1  10289  itunitc1  10356  axdc3lem2  10387  ttukeylem1  10445  fpwwe2cbv  10566  fpwwe2lem2  10568  fpwwe2  10579  fpwwecbv  10580  fpwwelem  10581  canthwelem  10586  canthwe  10587  wunex2  10674  wuncval2  10683  eltsk2g  10687  tskpwss  10688  inar1  10711  grothpw  10762  grothpwex  10763  axgroth6  10764  grothac  10766  peano5uzti  12593  fsuppmapnn0fiub0  13898  relexpnndm  14926  rtrclreclem4  14946  dfrtrcl2  14947  lo1o1  15414  o1lo1  15419  o1lo12  15420  lo1eq  15450  rlimeq  15451  isercoll  15552  prmreclem4  16791  vdwmc  16850  vdwlem1  16853  vdwlem2  16854  vdwlem12  16864  vdwlem13  16865  ramval  16880  ramz2  16896  ramub1lem1  16898  isacs2  17533  isacs1i  17537  mreacs  17538  acsfn  17539  rescabs  17718  rescabsOLD  17719  ipole  18423  ipodrsima  18430  isacs5  18437  symgsssg  19249  psgnunilem5  19276  sylow1  19385  efgval2  19506  efgsfo  19521  frgpuplem  19554  gsumzf1o  19689  gsumzoppg  19721  dprdcntz  19787  islbs2  20615  frlmssuvc1  21200  frlmssuvc2  21201  frlmsslsp  21202  ismhp  21531  pptbas  22358  pnfnei  22571  mnfnei  22572  iscnp  22588  iscnp4  22614  cnntr  22626  cnconst2  22634  cnpresti  22639  cnprest  22640  isreg  22683  isnrm  22686  isnrm2  22709  perfcls  22716  isreg2  22728  hauscmplem  22757  1stcfb  22796  1stcelcls  22812  1stccnp  22813  txbas  22918  ptbasfi  22932  xkoopn  22940  xkoccn  22970  txcnp  22971  ptcnplem  22972  txdis  22983  txdis1cn  22986  txtube  22991  txkgen  23003  xkohaus  23004  xkoptsub  23005  xkoco1cn  23008  xkoco2cn  23009  xkococnlem  23010  xkococn  23011  xkoinjcn  23038  kqreglem1  23092  kqreglem2  23093  kqnrmlem1  23094  kqnrmlem2  23095  reghmph  23144  nrmhmph  23145  trfil2  23238  ufileu  23270  elfm  23298  elfm2  23299  elfm3  23301  imaelfm  23302  rnelfm  23304  fmfnfmlem2  23306  fmfnfmlem4  23308  fmco  23312  elflim2  23315  flffbas  23346  lmflf  23356  txflf  23357  fclscf  23376  flimfnfcls  23379  cnextcn  23418  symgtgp  23457  ghmcnp  23466  qustgplem  23472  eltsms  23484  ustval  23554  ust0  23571  trust  23581  utoptop  23586  restutop  23589  restutopopn  23590  utopsnneiplem  23599  ucncn  23637  fmucnd  23644  cfilufg  23645  trcfilu  23646  neipcfilu  23648  blssps  23777  blss  23778  ssblex  23781  blin2  23782  metss2  23868  metrest  23880  metcnp3  23896  metustexhalf  23912  metustbl  23922  psmetutop  23923  xrsmopn  24175  recld2  24177  icccmplem1  24185  icccmplem2  24186  icccmp  24188  reconnlem2  24190  lebnumlem3  24326  lebnum  24327  xlebnum  24328  lebnumii  24329  nmhmcn  24483  cfilfval  24628  caubl  24672  caublcls  24673  bcthlem1  24688  bcth  24693  ovolfiniun  24865  ovoliunlem3  24868  ovoliun  24869  ovoliun2  24870  ovoliunnul  24871  voliunlem3  24916  dyadmax  24962  dyadmbllem  24963  dyadmbl  24964  opnmbllem  24965  ellimc2  25241  limcnlp  25242  ellimc3  25243  limcflf  25245  limciun  25258  cpnord  25299  lhop  25380  xrlimcnp  26318  cvxcl  26334  dchrval  26582  noetalem2  27090  madebdayim  27217  madebdaylemold  27227  madebday  27229  ausgrumgri  28118  ausgrusgri  28119  nbgrval  28284  nbgrel  28288  nbumgrvtx  28294  nbgrnself  28307  uvtxel1  28344  wlkonl1iedg  28613  crctcshwlkn0lem6  28760  2wlkdlem10  28880  1wlkdlem4  29084  3wlkdlem6  29109  3wlkdlem10  29113  eupth2lem3lem4  29175  frcond1  29210  frgr1v  29215  nfrgr2v  29216  frgr3vlem1  29217  frgr3vlem2  29218  frgr3v  29219  4cycl2vnunb  29234  n4cyclfrgr  29235  isssp  29666  ubthlem1  29812  shmodi  30332  chsupid  30354  chsscon3  30442  spansncvi  30594  mdslmd1lem3  31269  mdslmd1lem4  31270  mdsymlem5  31349  dmdbr5ati  31364  dmdbr6ati  31365  dmdbr7ati  31366  ssiun2sf  31478  fpwrelmapffslem  31649  pwrssmgc  31860  fldgenval  32081  txomap  32415  locfinreflem  32421  tpr2rico  32493  pnfneige0  32532  rrhre  32602  prodindf  32622  dya2icoseg2  32878  omsfval  32894  eulerpartlemt0  32969  eulerpartgbij  32972  eulerpartlemr  32974  eulerpartlemgs2  32980  eulerpartlemn  32981  eulerpart  32982  bnj517  33497  bnj1014  33573  bnj1015  33574  bnj1123  33598  bnj1125  33604  bnj1450  33662  bnj1452  33664  cplgredgex  33714  kur14  33810  cvmliftlem15  33892  cvmlift2lem12  33908  cvmlift2lem13  33909  mclsval  34157  mclsax  34163  mclsppslem  34177  opnrebl  34792  opnrebl2  34793  ivthALT  34807  neibastop2lem  34832  fnemeet1  34838  filnetlem1  34850  filnetlem4  34853  bj-imdirval3  35655  bj-imdiridlem  35656  rdgssun  35849  lindsadd  36071  lindsenlbs  36073  ptrecube  36078  poimirlem32  36110  opnmbllem0  36114  mblfinlem1  36115  mblfinlem2  36116  mblfinlem3  36117  ovoliunnfl  36120  ex-ovoliunnfl  36121  voliunnfl  36122  totbndbnd  36248  heibor1lem  36268  heiborlem10  36279  scottexf  36627  scott0f  36628  relcnveq2  36784  cnvref4  36811  elrelscnveq2  36955  dfcnvrefrels2  36990  dfcnvrefrel2  36992  symrefref2  37025  lcv1  37503  lfl1dim  37583  lfl1dim2N  37584  paddasslem17  38299  dihglblem6  39803  dochvalr  39820  dochord3  39835  lpolconN  39950  lcfls1lem  39997  mapdffval  40089  mapdfval  40090  mapdsn2  40105  mapd0  40128  lspindp5  40233  mapdh8ab  40240  ismrcd1  41007  nacsfix  41021  setindtr  41334  hbtlem6  41442  clcnvlem  41885  iunrelexpmin1  41970  iunrelexpmin2  41974  relexp0a  41978  cotrcltrcl  41987  trclimalb2  41988  cotrclrcl  42004  sbcheg  42041  clsk1indlem1  42307  isotone1  42310  isotone2  42311  ntrclsiso  42329  ntrclsk2  42330  k0004lem1  42409  k0004lem3  42411  scottelrankd  42517  mnuop123d  42532  mnuprdlem1  42542  mnuprdlem2  42543  mnuunid  42547  mnurndlem1  42551  ssdec  43288  iinssd  43331  iinssdf  43339  ssnnf1octb  43404  iooiinicc  43770  iooiinioc  43784  icccncfext  44118  fourierdlem41  44379  meaiininclem  44717  hoidmvlelem3  44828  hoidmvle  44831  opnvonmbllem1  44863  opnvonmbl  44865  iinhoiicclem  44904  smflim  45008  smflimsuplem7  45057  uspgrsprf  46038  iscnrm3r  46971  iscnrm3l  46974  setrecseq  47120  setrec1lem4  47125  setrec2fun  47127