Theorem fneq2d 6020

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fn 5929

This theorem is referenced by:  fneq12d  6021  fnprb  6513  fntpb  6514  fnpr2g  6515  undifixp  7986  brwdom2  8519  dfac3  8982  ac7g  9334  ccatlid  13404  ccatrid  13405  ccatass  13406  ccatswrd  13502  swrdccat2  13504  swrdswrd  13506  swrdccatin2  13533  swrdccatin12  13537  revccat  13561  revrev  13562  repsdf2  13571  0csh0  13585  cshco  13628  wrd2pr2op  13733  wrd3tpop  13737  ofccat  13754  seqshft  13869  invf  16475  sscfn1  16524  sscfn2  16525  isssc  16527  fuchom  16668  estrchomfeqhom  16823  mulgfval  17589  symgplusg  17855  subrgascl  19546  frlmsslss2  20162  m1detdiag  20451  ptval  21421  xpsdsfn2  22230  fresf1o  29561  psgndmfi  29974  pl1cn  30129  signsvtn0  30775  signstres  30780  bnj927  30965  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  dibfnN  36762  dihintcl  36950  uzmptshftfval  38862  ccatpfx  41734  pfxccatin12  41750  srhmsubc  42401  srhmsubcALTV  42419