Theorem fneq2d 6630

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 6628	. 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 6532

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 2155  ax-ext 2734

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

This theorem is used by:  fneq12d  6631  fncofn  6653  fnco  6654  fnprb  7211  fntpb  7212  fnpr2g  7213  undifixp  8945  brwdom2  9549  brttrcl2  9697  ssttrcl  9698  ttrcltr  9699  ttrclss  9703  ttrclselem2  9709  dfac3  10128  ac7g  10480  ccatlid  14656  ccatrid  14657  ccatass  14658  ccatswrd  14742  swrdccat2  14743  ccatpfx  14774  swrdswrd  14778  swrdccatin2  14802  pfxccatin12  14806  revccat  14839  revrev  14840  revpfxsfxrev  14841  repsdf2  14853  0csh0  14868  cshco  14911  wrd2pr2op  15018  wrd3tpop  15023  ofccat  15046  seqshft  15162  invf  17863  sscfn1  17912  sscfn2  17913  isssc  17915  fuchom  18059  estrchomfeqhom  18230  mulgfval  19198  mulgfvalALT  19199  srhmsubc  20848  frlmsslss2  21994  subrgascl  22288  selvvvval  22364  m1detdiag  22825  ptval  23802  xpsdsfn2  24610  fresf1o  33112  psgndmfi  33546  cycpmconjslem1  33602  cycpmconjslem2  33603  ply1annidllem  34219  pl1cn  34473  signsvtn0  35086  signstres  35091  bnj927  35287  fineqvac  35650  ixpeq12dv  36844  cbvixpdavw  36906  cbvixpdavw2  36922  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  dibfnN  42037  dihintcl  42225  frlmvscadiccat  43402  ofoafg  44203  uzmptshftfval  45178  srhmsubcALTV  49248  tposideq  49822  nelsubc3lem  50004  0funcg2  50018  fucofulem2  50245  termcfuncval  50466  termcnatval  50469  0fucterm  50477  cnelsubclem  50537