Theorem fneq1i 6023

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

Syntax hints:   ↔ wb 196   = wceq 1523   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-fun 5928  df-fn 5929

This theorem is referenced by:  fnunsn  6036  mptfnf  6053  fnopabg  6055  f1oun  6194  f1oi  6212  f1osn  6214  ovid  6819  curry1  7314  curry2  7317  wfrlem5  7464  wfrlem13  7472  tfrlem10  7528  tfr1  7538  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  fnseqom  7595  unblem4  8256  r1fnon  8668  alephfnon  8926  alephfplem4  8968  alephfp  8969  cfsmolem  9130  infpssrlem3  9165  compssiso  9234  hsmexlem5  9290  axdclem2  9380  wunex2  9598  wuncval2  9607  om2uzrani  12791  om2uzf1oi  12792  uzrdglem  12796  uzrdgfni  12797  uzrdg0i  12798  hashkf  13159  dmaf  16746  cdaf  16747  prdsinvlem  17571  srg1zr  18575  pws1  18662  frlmphl  20168  ovolunlem1  23311  0plef  23484  0pledm  23485  itg1ge0  23498  itg1addlem4  23511  mbfi1fseqlem5  23531  itg2addlem  23570  qaa  24123  0vfval  27589  xrge0pluscn  30114  bnj927  30965  bnj535  31086  frrlem5  31909  fullfunfnv  32178  neibastop2lem  32480  fourierdlem42  40684  rngcrescrhm  42410  rngcrescrhmALTV  42428