Theorem fneq2d 6633

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 6631	. 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 6533

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 2733

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

This theorem is used by:  fneq12d  6634  fncofn  6656  fnco  6657  fnprb  7214  fntpb  7215  fnpr2g  7216  undifixp  8962  brwdom2  9567  brttrcl2  9715  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  dfac3  10200  ac7g  10552  ccatlid  14732  ccatrid  14733  ccatass  14734  ccatswrd  14818  swrdccat2  14819  ccatpfx  14850  swrdswrd  14854  swrdccatin2  14878  pfxccatin12  14882  revccat  14915  revrev  14916  revpfxsfxrev  14917  repsdf2  14929  0csh0  14944  cshco  14987  wrd2pr2op  15094  wrd3tpop  15099  ofccat  15122  seqshft  15238  invf  17943  sscfn1  17992  sscfn2  17993  isssc  17995  fuchom  18139  estrchomfeqhom  18310  mulgfval  19279  mulgfvalALT  19280  srhmsubc  20932  frlmsslss2  22081  subrgascl  22375  selvvvval  22451  m1detdiag  22912  ptval  23889  xpsdsfn2  24697  fresf1o  33225  psgndmfi  33659  cycpmconjslem1  33715  cycpmconjslem2  33716  ply1annidllem  34333  pl1cn  34587  signsvtn0  35199  signstres  35204  bnj927  35400  fineqvac  35784  ixpeq12dv  37005  cbvixpdavw  37067  cbvixpdavw2  37083  poimirlem1  38540  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem11  38550  poimirlem12  38551  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  dibfnN  42214  dihintcl  42402  frlmvscadiccat  43574  ofoafg  44356  uzmptshftfval  45330  srhmsubcALTV  49422  tposideq  49996  nelsubc3lem  50178  0funcg2  50192  fucofulem2  50419  termcfuncval  50640  termcnatval  50643  0fucterm  50651  cnelsubclem  50711