Theorem fneq2d 6632

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   Fn wfn 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-fn 6534

This theorem is referenced by:  fneq12d  6633  fncofn  6655  fnco  6656  fnprb  7200  fntpb  7201  fnpr2g  7202  undifixp  8948  brwdom2  9587  brttrcl2  9728  ssttrcl  9729  ttrcltr  9730  ttrclss  9734  ttrclselem2  9740  dfac3  10135  ac7g  10488  ccatlid  14604  ccatrid  14605  ccatass  14606  ccatswrd  14686  swrdccat2  14687  ccatpfx  14719  swrdswrd  14723  swrdccatin2  14747  pfxccatin12  14751  revccat  14784  revrev  14785  repsdf2  14796  0csh0  14811  cshco  14855  wrd2pr2op  14962  wrd3tpop  14967  ofccat  14988  seqshft  15104  invf  17781  sscfn1  17830  sscfn2  17831  isssc  17833  fuchom  17977  estrchomfeqhom  18148  mulgfval  19052  mulgfvalALT  19053  srhmsubc  20640  frlmsslss2  21735  subrgascl  22024  m1detdiag  22535  ptval  23508  xpsdsfn2  24317  fresf1o  32609  psgndmfi  33109  cycpmconjslem1  33165  cycpmconjslem2  33166  ply1annidllem  33735  pl1cn  33986  signsvtn0  34602  signstres  34607  bnj927  34800  fineqvac  35128  revpfxsfxrev  35138  ixpeq12dv  36234  cbvixpdavw  36296  cbvixpdavw2  36312  poimirlem1  37645  poimirlem2  37646  poimirlem3  37647  poimirlem4  37648  poimirlem6  37650  poimirlem7  37651  poimirlem11  37655  poimirlem12  37656  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  dibfnN  41175  dihintcl  41363  frlmvscadiccat  42529  selvvvval  42608  ofoafg  43378  uzmptshftfval  44370  srhmsubcALTV  48300  tposideq  48863  nelsubc3lem  49037  0funcg2  49049  fucofulem2  49222  termcfuncval  49417  termcnatval  49420  cnelsubclem  49480