Theorem fneq2d 6643

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fneq2d	⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Proof of Theorem fneq2d

Step	Hyp	Ref	Expression
1		fneq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fneq2 6641	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   Fn wfn 6538

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6546

This theorem is referenced by:  fneq12d  6644  fncofn  6666  fnco  6667  fnprb  7212  fntpb  7213  fnpr2g  7214  undifixp  8934  brwdom2  9574  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  dfac3  10122  ac7g  10475  ccatlid  14543  ccatrid  14544  ccatass  14545  ccatswrd  14625  swrdccat2  14626  ccatpfx  14658  swrdswrd  14662  swrdccatin2  14686  pfxccatin12  14690  revccat  14723  revrev  14724  repsdf2  14735  0csh0  14750  cshco  14794  wrd2pr2op  14901  wrd3tpop  14906  ofccat  14923  seqshft  15039  invf  17722  sscfn1  17771  sscfn2  17772  isssc  17774  fuchom  17923  fuchomOLD  17924  estrchomfeqhom  18097  mulgfval  18995  mulgfvalALT  18996  srhmsubc  20572  frlmsslss2  21641  subrgascl  21939  m1detdiag  22420  ptval  23395  xpsdsfn2  24205  fresf1o  32290  psgndmfi  32695  cycpmconjslem1  32751  cycpmconjslem2  32752  ply1annidllem  33219  pl1cn  33401  signsvtn0  34047  signstres  34052  bnj927  34246  fineqvac  34563  revpfxsfxrev  34572  poimirlem1  36956  poimirlem2  36957  poimirlem3  36958  poimirlem4  36959  poimirlem6  36961  poimirlem7  36962  poimirlem11  36966  poimirlem12  36967  poimirlem16  36971  poimirlem17  36972  poimirlem19  36974  poimirlem20  36975  dibfnN  40494  dihintcl  40682  frlmvscadiccat  41550  selvvvval  41623  ofoafg  42570  uzmptshftfval  43571  srhmsubcALTV  47165