Theorem fneq1i 6635

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 6629	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1540   Fn wfn 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-fun 6533  df-fn 6534

This theorem is referenced by:  fnunop  6654  mptfnf  6673  fnopabg  6675  f1oun  6837  f1oi  6856  f1osn  6858  ovid  7548  curry1  8103  curry2  8106  fsplitfpar  8117  frrlem11  8295  wfrlem5OLD  8327  wfrlem13OLD  8335  tfrlem10  8401  tfr1  8411  seqomlem2  8465  seqomlem3  8466  seqomlem4  8467  fnseqom  8469  unblem4  9303  r1fnon  9781  alephfnon  10079  alephfplem4  10121  alephfp  10122  cfsmolem  10284  infpssrlem3  10319  compssiso  10388  hsmexlem5  10444  axdclem2  10534  wunex2  10752  wuncval2  10761  om2uzrani  13970  om2uzf1oi  13971  uzrdglem  13975  uzrdgfni  13976  uzrdg0i  13977  hashkf  14350  dmaf  18062  cdaf  18063  prdsinvlem  19032  srg1zr  20175  pws1  20285  rngcrescrhm  20644  frlmphl  21741  ovolunlem1  25450  0plef  25625  0pledm  25626  itg1ge0  25639  mbfi1fseqlem5  25672  itg2addlem  25711  qaa  26283  precsexlem1  28161  precsexlem2  28162  precsexlem3  28163  precsexlem4  28164  precsexlem5  28165  ex-fpar  30443  0vfval  30587  xrge0pluscn  33971  bnj927  34800  bnj535  34921  fullfunfnv  35964  neibastop2lem  36378  fnmptif  45289  fourierdlem42  46178  fcoreslem4  47095  upgrimwlklem1  47910  rngcrescrhmALTV  48255  isofval2  49002