Theorem fneq2d 6592

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   Fn wfn 6493

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501

This theorem is referenced by:  fneq12d  6593  fncofn  6615  fnco  6616  fnprb  7163  fntpb  7164  fnpr2g  7165  undifixp  8882  brwdom2  9488  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  dfac3  10043  ac7g  10396  ccatlid  14549  ccatrid  14550  ccatass  14551  ccatswrd  14631  swrdccat2  14632  ccatpfx  14663  swrdswrd  14667  swrdccatin2  14691  pfxccatin12  14695  revccat  14728  revrev  14729  repsdf2  14740  0csh0  14755  cshco  14798  wrd2pr2op  14905  wrd3tpop  14910  ofccat  14931  seqshft  15047  invf  17735  sscfn1  17784  sscfn2  17785  isssc  17787  fuchom  17931  estrchomfeqhom  18102  mulgfval  19045  mulgfvalALT  19046  srhmsubc  20657  frlmsslss2  21755  subrgascl  22044  m1detdiag  22562  ptval  23535  xpsdsfn2  24343  fresf1o  32704  psgndmfi  33159  cycpmconjslem1  33215  cycpmconjslem2  33216  ply1annidllem  33845  pl1cn  34099  signsvtn0  34714  signstres  34719  bnj927  34912  fineqvac  35260  revpfxsfxrev  35298  ixpeq12dv  36398  cbvixpdavw  36460  cbvixpdavw2  36476  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  dibfnN  41602  dihintcl  41790  frlmvscadiccat  42951  selvvvval  43018  ofoafg  43782  uzmptshftfval  44773  srhmsubcALTV  48801  tposideq  49363  nelsubc3lem  49545  0funcg2  49559  fucofulem2  49786  termcfuncval  50007  termcnatval  50010  0fucterm  50018  cnelsubclem  50078