Theorem fneq1i 6652

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

Syntax hints:   ↔ wb 205   = wceq 1533   Fn wfn 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-fun 6551  df-fn 6552

This theorem is referenced by:  fnunop  6671  mptfnf  6691  fnopabg  6693  f1oun  6857  f1oi  6876  f1osn  6878  ovid  7562  curry1  8109  curry2  8112  fsplitfpar  8123  frrlem11  8302  wfrlem5OLD  8334  wfrlem13OLD  8342  tfrlem10  8408  tfr1  8418  seqomlem2  8472  seqomlem3  8473  seqomlem4  8474  fnseqom  8476  unblem4  9323  r1fnon  9792  alephfnon  10090  alephfplem4  10132  alephfp  10133  cfsmolem  10295  infpssrlem3  10330  compssiso  10399  hsmexlem5  10455  axdclem2  10545  wunex2  10763  wuncval2  10772  om2uzrani  13953  om2uzf1oi  13954  uzrdglem  13958  uzrdgfni  13959  uzrdg0i  13960  hashkf  14327  dmaf  18041  cdaf  18042  prdsinvlem  19013  srg1zr  20167  pws1  20273  rngcrescrhm  20629  frlmphl  21732  ovolunlem1  25470  0plef  25645  0pledm  25646  itg1ge0  25659  itg1addlem4OLD  25673  mbfi1fseqlem5  25693  itg2addlem  25732  qaa  26303  precsexlem1  28155  precsexlem2  28156  precsexlem3  28157  precsexlem4  28158  precsexlem5  28159  ex-fpar  30344  0vfval  30488  xrge0pluscn  33672  bnj927  34531  bnj535  34652  fullfunfnv  35673  neibastop2lem  35975  fnmptif  44780  fourierdlem42  45675  fcoreslem4  46586  rngcrescrhmALTV  47528