Theorem fneq2d 6586

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495

This theorem is referenced by:  fneq12d  6587  fncofn  6609  fnco  6610  fnprb  7159  fntpb  7160  fnpr2g  7161  undifixp  8879  brwdom2  9485  brttrcl2  9633  ssttrcl  9634  ttrcltr  9635  ttrclss  9639  ttrclselem2  9645  dfac3  10041  ac7g  10394  ccatlid  14547  ccatrid  14548  ccatass  14549  ccatswrd  14629  swrdccat2  14630  ccatpfx  14661  swrdswrd  14665  swrdccatin2  14689  pfxccatin12  14693  revccat  14726  revrev  14727  repsdf2  14738  0csh0  14753  cshco  14796  wrd2pr2op  14903  wrd3tpop  14908  ofccat  14929  seqshft  15045  invf  17733  sscfn1  17782  sscfn2  17783  isssc  17785  fuchom  17929  estrchomfeqhom  18100  mulgfval  19043  mulgfvalALT  19044  srhmsubc  20659  frlmsslss2  21757  subrgascl  22049  selvvvval  22125  m1detdiag  22587  ptval  23560  xpsdsfn2  24368  fresf1o  32730  psgndmfi  33186  cycpmconjslem1  33242  cycpmconjslem2  33243  ply1annidllem  33892  pl1cn  34146  signsvtn0  34761  signstres  34766  bnj927  34959  fineqvac  35304  revpfxsfxrev  35351  ixpeq12dv  36451  cbvixpdavw  36513  cbvixpdavw2  36529  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  dibfnN  41655  dihintcl  41843  frlmvscadiccat  43003  ofoafg  43806  uzmptshftfval  44797  srhmsubcALTV  48823  tposideq  49385  nelsubc3lem  49567  0funcg2  49581  fucofulem2  49808  termcfuncval  50029  termcnatval  50032  0fucterm  50040  cnelsubclem  50100