Theorem fneq1 6583

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fneq1	⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Proof of Theorem fneq1

Step	Hyp	Ref	Expression
1		funeq 6512	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5852	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2739	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6495	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6495	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fneq1d  6585  fneq1i  6589  fn0  6623  feq1  6640  foeq1  6742  f1ocnv  6786  dffn5  6892  mpteqb  6961  fnsnbg  7112  fnsnbOLD  7114  fnprb  7156  fntpb  7157  eufnfv  7177  frrlem1  8229  frrlem13  8241  tfrlem12  8321  fsetdmprc0  8795  mapval2  8813  elixp2  8842  ixpfn  8844  elixpsn  8878  inf3lem6  9545  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  aceq3lem  10033  dfac4  10035  dfacacn  10055  axcc2lem  10349  axcc3  10351  seqof  14012  ccatvalfn  14534  cshword  14744  0csh0  14746  rrgsupp  20669  lmodfopnelem1  20884  elpt  23547  elptr  23548  ptcmplem3  24029  prdsxmslem2  24504  tgjustr  28556  esplyind  33734  bnj62  34879  bnj976  34936  bnj66  35018  bnj124  35029  bnj607  35074  bnj873  35082  bnj1234  35171  bnj1463  35213  fineqvac  35276  fineqvnttrclse  35284  gblacfnacd  35300  eqresfnbd  42687  dssmapf1od  44466  fnchoice  45478  choicefi  45647  axccdom  45669  dfafn5b  47621  rngchomffvalALTV  48766  ixpv  49377  iinfconstbaslem  49552  iinfconstbas  49553  nelsubc3lem  49557  functhinclem1  49931  cnelsubclem  50090