Theorem fneq2d 6428

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   Fn wfn 6330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-fn 6338

This theorem is referenced by:  fneq12d  6429  fnprb  6962  fntpb  6963  fnpr2g  6964  undifixp  8516  brwdom2  9070  dfac3  9581  ac7g  9934  ccatlid  13987  ccatrid  13988  ccatass  13989  ccatswrd  14077  swrdccat2  14078  ccatpfx  14110  swrdswrd  14114  swrdccatin2  14138  pfxccatin12  14142  revccat  14175  revrev  14176  repsdf2  14187  0csh0  14202  cshco  14245  wrd2pr2op  14352  wrd3tpop  14357  ofccat  14376  seqshft  14492  invf  17097  sscfn1  17146  sscfn2  17147  isssc  17149  fuchom  17290  estrchomfeqhom  17452  mulgfval  18293  mulgfvalALT  18294  frlmsslss2  20540  subrgascl  20827  m1detdiag  21297  ptval  22270  xpsdsfn2  23080  fresf1o  30488  psgndmfi  30891  cycpmconjslem1  30947  cycpmconjslem2  30948  pl1cn  31426  signsvtn0  32068  signstres  32073  bnj927  32268  revpfxsfxrev  32593  poimirlem1  35338  poimirlem2  35339  poimirlem3  35340  poimirlem4  35341  poimirlem6  35343  poimirlem7  35344  poimirlem11  35348  poimirlem12  35349  poimirlem16  35353  poimirlem17  35354  poimirlem19  35356  poimirlem20  35357  dibfnN  38732  dihintcl  38920  frlmvscadiccat  39744  uzmptshftfval  41423  srhmsubc  45067  srhmsubcALTV  45085