Theorem fneq2d 6229

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   Fn wfn 6132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-fn 6140

This theorem is referenced by:  fneq12d  6230  fnprb  6746  fntpb  6747  fnpr2g  6748  undifixp  8232  brwdom2  8769  dfac3  9279  ac7g  9633  ccatlid  13680  ccatrid  13681  ccatass  13682  ccatswrd  13780  swrdccat2  13782  ccatpfx  13814  swrdswrd  13818  swrdccatin2  13860  pfxccatin12  13865  swrdccatin12OLD  13866  revccat  13916  revrev  13917  repsdf2  13928  0csh0  13947  0csh0OLD  13948  cshco  13991  wrd2pr2op  14098  wrd3tpop  14103  ofccat  14121  seqshft  14236  invf  16817  sscfn1  16866  sscfn2  16867  isssc  16869  fuchom  17010  estrchomfeqhom  17165  mulgfval  17933  symgplusg  18196  subrgascl  19898  frlmsslss2  20522  m1detdiag  20812  ptval  21786  xpsdsfn2  22595  fresf1o  30002  psgndmfi  30448  pl1cn  30603  signsvtn0  31251  signsvtn0OLD  31252  signstres  31257  bnj927  31442  poimirlem1  34041  poimirlem2  34042  poimirlem3  34043  poimirlem4  34044  poimirlem6  34046  poimirlem7  34047  poimirlem11  34051  poimirlem12  34052  poimirlem16  34056  poimirlem17  34057  poimirlem19  34059  poimirlem20  34060  dibfnN  37315  dihintcl  37503  uzmptshftfval  39511  srhmsubc  43101  srhmsubcALTV  43119