Theorem fneq1i 6647

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

Syntax hints:   ↔ wb 205   = wceq 1542   Fn wfn 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-fun 6546  df-fn 6547

This theorem is referenced by:  fnunop  6666  mptfnf  6686  fnopabg  6688  f1oun  6853  f1oi  6872  f1osn  6874  ovid  7549  curry1  8090  curry2  8093  fsplitfpar  8104  frrlem11  8281  wfrlem5OLD  8313  wfrlem13OLD  8321  tfrlem10  8387  tfr1  8397  seqomlem2  8451  seqomlem3  8452  seqomlem4  8453  fnseqom  8455  unblem4  9298  r1fnon  9762  alephfnon  10060  alephfplem4  10102  alephfp  10103  cfsmolem  10265  infpssrlem3  10300  compssiso  10369  hsmexlem5  10425  axdclem2  10515  wunex2  10733  wuncval2  10742  om2uzrani  13917  om2uzf1oi  13918  uzrdglem  13922  uzrdgfni  13923  uzrdg0i  13924  hashkf  14292  dmaf  17999  cdaf  18000  prdsinvlem  18932  srg1zr  20038  pws1  20138  frlmphl  21336  ovolunlem1  25014  0plef  25189  0pledm  25190  itg1ge0  25203  itg1addlem4OLD  25217  mbfi1fseqlem5  25237  itg2addlem  25276  qaa  25836  precsexlem1  27653  precsexlem2  27654  precsexlem3  27655  precsexlem4  27656  precsexlem5  27657  ex-fpar  29715  0vfval  29859  xrge0pluscn  32920  bnj927  33780  bnj535  33901  fullfunfnv  34918  neibastop2lem  35245  fnmptif  43970  fourierdlem42  44865  fcoreslem4  45776  rngcrescrhm  46983  rngcrescrhmALTV  47001