Theorem fneq1i 6646

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

Syntax hints:   ↔ wb 205   = wceq 1541   Fn wfn 6538

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-fun 6545  df-fn 6546

This theorem is referenced by:  fnunop  6665  mptfnf  6685  fnopabg  6687  f1oun  6852  f1oi  6871  f1osn  6873  ovid  7551  curry1  8092  curry2  8095  fsplitfpar  8106  frrlem11  8283  wfrlem5OLD  8315  wfrlem13OLD  8323  tfrlem10  8389  tfr1  8399  seqomlem2  8453  seqomlem3  8454  seqomlem4  8455  fnseqom  8457  unblem4  9300  r1fnon  9764  alephfnon  10062  alephfplem4  10104  alephfp  10105  cfsmolem  10267  infpssrlem3  10302  compssiso  10371  hsmexlem5  10427  axdclem2  10517  wunex2  10735  wuncval2  10744  om2uzrani  13921  om2uzf1oi  13922  uzrdglem  13926  uzrdgfni  13927  uzrdg0i  13928  hashkf  14296  dmaf  18003  cdaf  18004  prdsinvlem  18968  srg1zr  20109  pws1  20213  frlmphl  21555  ovolunlem1  25238  0plef  25413  0pledm  25414  itg1ge0  25427  itg1addlem4OLD  25441  mbfi1fseqlem5  25461  itg2addlem  25500  qaa  26060  precsexlem1  27880  precsexlem2  27881  precsexlem3  27882  precsexlem4  27883  precsexlem5  27884  ex-fpar  29970  0vfval  30114  xrge0pluscn  33206  bnj927  34066  bnj535  34187  fullfunfnv  35210  neibastop2lem  35548  fnmptif  44269  fourierdlem42  45164  fcoreslem4  46075  rngcrescrhm  47072  rngcrescrhmALTV  47090