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 206   = wceq 1542   Fn wfn 6487

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 2709

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

This theorem is referenced by:  fneq12d  6587  fncofn  6609  fnco  6610  fnprb  7156  fntpb  7157  fnpr2g  7158  undifixp  8875  brwdom2  9481  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  dfac3  10034  ac7g  10387  ccatlid  14540  ccatrid  14541  ccatass  14542  ccatswrd  14622  swrdccat2  14623  ccatpfx  14654  swrdswrd  14658  swrdccatin2  14682  pfxccatin12  14686  revccat  14719  revrev  14720  repsdf2  14731  0csh0  14746  cshco  14789  wrd2pr2op  14896  wrd3tpop  14901  ofccat  14922  seqshft  15038  invf  17726  sscfn1  17775  sscfn2  17776  isssc  17778  fuchom  17922  estrchomfeqhom  18093  mulgfval  19036  mulgfvalALT  19037  srhmsubc  20648  frlmsslss2  21765  subrgascl  22054  m1detdiag  22572  ptval  23545  xpsdsfn2  24353  fresf1o  32719  psgndmfi  33174  cycpmconjslem1  33230  cycpmconjslem2  33231  ply1annidllem  33861  pl1cn  34115  signsvtn0  34730  signstres  34735  bnj927  34928  fineqvac  35276  revpfxsfxrev  35314  ixpeq12dv  36414  cbvixpdavw  36476  cbvixpdavw2  36492  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  dibfnN  41616  dihintcl  41804  frlmvscadiccat  42965  selvvvval  43032  ofoafg  43800  uzmptshftfval  44791  srhmsubcALTV  48813  tposideq  49375  nelsubc3lem  49557  0funcg2  49571  fucofulem2  49798  termcfuncval  50019  termcnatval  50022  0fucterm  50030  cnelsubclem  50090