Theorem fneq1i 6222

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

Syntax hints:   ↔ wb 198   = wceq 1656   Fn wfn 6122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876  df-opab 4938  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-fun 6129  df-fn 6130

This theorem is referenced by:  fnunsn  6235  mptfnf  6252  fnopabg  6254  f1oun  6401  f1oi  6419  f1osn  6421  ovid  7042  curry1  7538  curry2  7541  wfrlem5  7690  wfrlem13  7698  tfrlem10  7754  tfr1  7764  seqomlem2  7817  seqomlem3  7818  seqomlem4  7819  fnseqom  7821  unblem4  8490  r1fnon  8914  alephfnon  9208  alephfplem4  9250  alephfp  9251  cfsmolem  9414  infpssrlem3  9449  compssiso  9518  hsmexlem5  9574  axdclem2  9664  wunex2  9882  wuncval2  9891  om2uzrani  13053  om2uzf1oi  13054  uzrdglem  13058  uzrdgfni  13059  uzrdg0i  13060  hashkf  13419  dmaf  17058  cdaf  17059  prdsinvlem  17885  srg1zr  18890  pws1  18977  frlmphl  20494  ovolunlem1  23670  0plef  23845  0pledm  23846  itg1ge0  23859  itg1addlem4  23872  mbfi1fseqlem5  23892  itg2addlem  23931  qaa  24484  0vfval  28012  xrge0pluscn  30527  bnj927  31381  bnj535  31502  frrlem5  32318  fullfunfnv  32587  neibastop2lem  32888  fourierdlem42  41154  rngcrescrhm  42946  rngcrescrhmALTV  42964