Theorem fneq1i 6665

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-fun 6563  df-fn 6564

This theorem is referenced by:  fnunop  6684  mptfnf  6703  fnopabg  6705  f1oun  6867  f1oi  6886  f1osn  6888  ovid  7574  curry1  8129  curry2  8132  fsplitfpar  8143  frrlem11  8321  wfrlem5OLD  8353  wfrlem13OLD  8361  tfrlem10  8427  tfr1  8437  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  fnseqom  8495  unblem4  9331  r1fnon  9807  alephfnon  10105  alephfplem4  10147  alephfp  10148  cfsmolem  10310  infpssrlem3  10345  compssiso  10414  hsmexlem5  10470  axdclem2  10560  wunex2  10778  wuncval2  10787  om2uzrani  13993  om2uzf1oi  13994  uzrdglem  13998  uzrdgfni  13999  uzrdg0i  14000  hashkf  14371  dmaf  18094  cdaf  18095  prdsinvlem  19067  srg1zr  20212  pws1  20322  rngcrescrhm  20684  frlmphl  21801  ovolunlem1  25532  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  itg2addlem  25793  qaa  26365  precsexlem1  28231  precsexlem2  28232  precsexlem3  28233  precsexlem4  28234  precsexlem5  28235  ex-fpar  30481  0vfval  30625  xrge0pluscn  33939  bnj927  34783  bnj535  34904  fullfunfnv  35947  neibastop2lem  36361  fnmptif  45272  fourierdlem42  46164  fcoreslem4  47078  rngcrescrhmALTV  48196