Theorem fneq1i 6589

Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fneq1i	⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Proof of Theorem fneq1i

Step	Hyp	Ref	Expression
1		fneq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fneq1 6583	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Syntax hints:   ↔ 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-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnunop  6608  mptfnf  6627  fnopabg  6629  f1oun  6793  f1oiOLD  6813  f1osn  6815  ovid  7501  curry1  8047  curry2  8050  fsplitfpar  8061  frrlem11  8239  tfrlem10  8319  tfr1  8329  seqomlem2  8383  seqomlem3  8384  seqomlem4  8385  fnseqom  8387  unblem4  9198  r1fnon  9682  alephfnon  9978  alephfplem4  10020  alephfp  10021  cfsmolem  10183  infpssrlem3  10218  compssiso  10287  hsmexlem5  10343  axdclem2  10433  wunex2  10652  wuncval2  10661  om2uzrani  13905  om2uzf1oi  13906  uzrdglem  13910  uzrdgfni  13911  uzrdg0i  13912  hashkf  14285  dmaf  18007  cdaf  18008  prdsinvlem  19016  srg1zr  20187  pws1  20295  rngcrescrhm  20652  frlmphl  21771  ovolunlem1  25474  0plef  25649  0pledm  25650  itg1ge0  25663  mbfi1fseqlem5  25696  itg2addlem  25735  qaa  26300  precsexlem1  28213  precsexlem2  28214  precsexlem3  28215  precsexlem4  28216  precsexlem5  28217  ex-fpar  30547  0vfval  30692  xrge0pluscn  34100  bnj927  34928  bnj535  35048  fullfunfnv  36144  neibastop2lem  36558  fnmptif  45712  fourierdlem42  46595  cjnpoly  47349  fcoreslem4  47526  upgrimwlklem1  48385  rngcrescrhmALTV  48768  isofval2  49519