Theorem fneq2d 6636

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-fn 6546

This theorem is used by:  fneq12d  6637  fncofn  6659  fnco  6660  fnprb  7213  fntpb  7214  fnpr2g  7215  undifixp  8941  brwdom2  9545  brttrcl2  9693  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  dfac3  10124  ac7g  10476  ccatlid  14644  ccatrid  14645  ccatass  14646  ccatswrd  14730  swrdccat2  14731  ccatpfx  14762  swrdswrd  14766  swrdccatin2  14790  pfxccatin12  14794  revccat  14827  revrev  14828  revpfxsfxrev  14829  repsdf2  14841  0csh0  14856  cshco  14899  wrd2pr2op  15006  wrd3tpop  15011  ofccat  15032  seqshft  15148  invf  17850  sscfn1  17899  sscfn2  17900  isssc  17902  fuchom  18046  estrchomfeqhom  18217  mulgfval  19166  mulgfvalALT  19167  srhmsubc  20816  frlmsslss2  21962  subrgascl  22254  selvvvval  22330  m1detdiag  22791  ptval  23764  xpsdsfn2  24572  fresf1o  33013  psgndmfi  33449  cycpmconjslem1  33505  cycpmconjslem2  33506  ply1annidllem  34122  pl1cn  34376  signsvtn0  34989  signstres  34994  bnj927  35190  fineqvac  35553  ixpeq12dv  36769  cbvixpdavw  36831  cbvixpdavw2  36847  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem11  38323  poimirlem12  38324  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  dibfnN  41971  dihintcl  42159  frlmvscadiccat  43321  ofoafg  44122  uzmptshftfval  45097  srhmsubcALTV  49131  tposideq  49707  nelsubc3lem  49889  0funcg2  49903  fucofulem2  50130  termcfuncval  50351  termcnatval  50354  0fucterm  50362  cnelsubclem  50422