Theorem fneq2d 5982

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891

This theorem is referenced by:  fneq12d  5983  fnprb  6472  fntpb  6473  fnpr2g  6474  undifixp  7944  brwdom2  8478  dfac3  8944  ac7g  9296  ccatlid  13369  ccatrid  13370  ccatass  13371  ccatswrd  13456  swrdccat2  13458  swrdswrd  13460  swrdccatin2  13487  swrdccatin12  13491  revccat  13515  revrev  13516  repsdf2  13525  0csh0  13539  cshco  13582  wrd2pr2op  13687  wrd3tpop  13691  ofccat  13708  seqshft  13825  invf  16428  sscfn1  16477  sscfn2  16478  isssc  16480  fuchom  16621  estrchomfeqhom  16776  mulgfval  17542  symgplusg  17809  subrgascl  19498  frlmsslss2  20114  m1detdiag  20403  ptval  21373  xpsdsfn2  22183  fresf1o  29433  psgndmfi  29846  pl1cn  30001  signsvtn0  30647  signstres  30652  bnj927  30839  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  dibfnN  36445  dihintcl  36633  uzmptshftfval  38545  ccatpfx  41409  pfxccatin12  41425  srhmsubc  42076  srhmsubcALTV  42094