MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2d Structured version   Visualization version   GIF version

Theorem feq2d 6209
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
feq2d (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 feq2 6205 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wf 6064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-fn 6071  df-f 6072
This theorem is referenced by:  feq12d  6211  ffdm  6244  fsng  6595  fsn2g  6596  fsnunf2  6645  issmo2  7650  qliftf  8038  elpm2r  8078  ralxpmap  8112  ordtypelem5  8634  axdc3lem3  9527  axdc3lem4  9528  fseq1p1m1  12621  fseq1m1p1  12622  seqf1o  13049  iswrdi  13490  wrdf  13491  wrdffz  13507  ffz0iswrd  13513  wrdnval  13516  ccatalpha  13564  swrdf  13627  swrd0fOLD  13629  cats1un  13719  cshwf  13829  wrdlen2i  13971  wwlktovf  13986  rlimi  14529  rlimmptrcl  14623  lo1mptrcl  14637  o1mptrcl  14638  o1fsum  14829  ram0  16005  funcres  16821  curf2cl  17137  uncfcurf  17145  yonedalem4c  17183  intopsn  17519  gsumprval  17547  resmhm  17625  gsumwsubmcl  17641  gsumccat  17644  gsumwmhm  17649  frmdup1  17668  frmdup3lem  17670  isghm  17924  resghm  17940  subgga  17996  gasubg  17998  psgnunilem2  18179  sylow2blem2  18300  pj2f  18375  pj1ghm  18380  frgpupf  18452  frgpup3lem  18456  gsumval3  18574  gsummptfzcl  18634  dprdf2  18673  ablfaclem2  18752  ablfac2  18755  isabvd  19089  abvpropd  19111  mplasclf  19770  evlssca  19795  lply1binomsc  19950  cygznlem2a  20188  frgpcyg  20194  mat1dimelbas  20554  mat2pmatbas  20810  cpmadugsumlemF  20960  cnpf2  21334  lmcnp  21388  ptpjcn  21694  cnextfres1  22151  cnextfres  22152  cnmpt2pc  23006  pi1addf  23125  pi1xfrf  23131  pi1cof  23137  mbfmptcl  23694  iblcnlem  23846  limcres  23941  cnplimc  23942  limccnp  23946  limccnp2  23947  limcun  23950  dvidlem  23970  cpnord  23989  dvaddf  23996  dvmulf  23997  dvcmulf  23999  dvcof  24002  dvcj  24004  dvrec  24009  dvmptcl  24013  dvcnvlem  24030  dvcnv  24031  rolle  24044  cmvth  24045  mvth  24046  dvlip  24047  dvlipcn  24048  c1lip2  24052  dv11cn  24055  dvivthlem1  24062  dvivthlem2  24063  dvivth  24064  dvne0  24065  lhop1lem  24067  lhop1  24068  lhop2  24069  lhop  24070  dvcnvrelem2  24072  taylthlem1  24418  taylthlem2  24419  ulmf2  24429  ulm2  24430  ulmdv  24448  pserdv  24474  rlimcxp  24991  o1cxp  24992  dchrptlem2  25281  axlowdimlem5  26117  axlowdimlem7  26119  axlowdimlem10  26122  uhgrn0  26239  wrdupgr  26257  upgrfn  26259  wrdumgr  26269  umgrfn  26271  upgr1e  26285  umgrres1  26485  upgr2wlk  26855  wlkres  26859  redwlklem  26860  wlkdlem1  26871  uhgrwkspthlem2  26942  usgr2wlkneq  26944  usgr2pthlem  26951  usgr2pth  26952  crctcshwlkn0  27006  wlkiswwlks2lem3  27062  wlkiswwlks2  27066  wlkiswwlksupgr2  27068  wlknewwlksn  27079  wpthswwlks2on  27185  clwlkclwwlklem2a  27225  clwlkclwwlklem1  27226  clwlksfclwwlk2wrdOLD  27333  clwlksfclwwlkOLD  27337  clwlksf1clwwlklem3OLD  27342  1wlkdlem1  27415  upgr3v3e3cycl  27458  upgr4cycl4dv4e  27463  isgrpo  27808  vciOLD  27872  isvclem  27888  isnvlem  27921  ajfval  28120  acunirnmpt2  29910  acunirnmpt2f  29911  smatrcl  30309  locfinref  30355  1stmbfm  30769  2ndmbfm  30770  sibfof  30849  rrvf2  30958  signshf  31116  reprsuc  31144  cvmliftmolem1  31711  cvmliftlem7  31721  cvmliftlem10  31724  cvmlift2lem9  31741  filnetlem4  32819  poimirlem16  33849  poimirlem19  33852  poimirlem23  33856  poimirlem24  33857  poimirlem25  33858  poimirlem29  33862  poimirlem31  33864  sdclem2  33960  sdclem1  33961  sdc  33962  fdc  33963  sstotbnd2  33995  elghomlem1OLD  34106  rngosn3  34145  amgm4d  39177  mptelpm  40004  fsneqrn  40048  cncfuni  40737  cncfiooicclem1  40744  dvsubf  40766  dvdivf  40775  dvbdfbdioolem1  40781  ioodvbdlimc1lem1  40784  ioodvbdlimc1lem2  40785  ioodvbdlimc1  40786  ioodvbdlimc2lem  40787  ioodvbdlimc2  40788  dvnprodlem3  40801  itgsubsticclem  40828  fourierdlem48  41008  fourierdlem49  41009  fourierdlem58  41018  fourierdlem59  41019  fourierdlem60  41020  fourierdlem61  41021  fourierdlem69  41029  fourierdlem75  41035  fourierdlem81  41041  fourierdlem89  41049  fourierdlem91  41051  fourierdlem97  41057  fourierdlem113  41073  meaf  41307  ismeannd  41321  psmeasure  41325  omef  41350  isomennd  41385  hoidmvlelem2  41450  hoidmvlelem3  41451  ovnhoi  41457  hspmbllem2  41481  sssmf  41587  smfpimioompt  41633  smffmpt  41651  2ffzoeq  42072  fargshiftf  42110  resmgmhm  42467  elbigolo1  43020
  Copyright terms: Public domain W3C validator