Theorem fneq1 6591

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 6520	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5860	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2739	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6503	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6503	. 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 5632  Fun wfun 6494   Fn wfn 6495

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  fneq1d  6593  fneq1i  6597  fn0  6631  feq1  6648  foeq1  6750  f1ocnv  6794  dffn5  6900  mpteqb  6969  fnsnbg  7120  fnsnbOLD  7122  fnprb  7164  fntpb  7165  eufnfv  7185  frrlem1  8238  frrlem13  8250  tfrlem12  8330  fsetdmprc0  8804  mapval2  8822  elixp2  8851  ixpfn  8853  elixpsn  8887  inf3lem6  9554  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  aceq3lem  10042  dfac4  10044  dfacacn  10064  axcc2lem  10358  axcc3  10360  seqof  13994  ccatvalfn  14516  cshword  14726  0csh0  14728  rrgsupp  20646  lmodfopnelem1  20861  elpt  23528  elptr  23529  ptcmplem3  24010  prdsxmslem2  24485  tgjustr  28558  esplyind  33751  bnj62  34896  bnj976  34953  bnj66  35035  bnj124  35046  bnj607  35091  bnj873  35099  bnj1234  35188  bnj1463  35230  fineqvac  35291  fineqvnttrclse  35299  gblacfnacd  35315  eqresfnbd  42601  dssmapf1od  44374  fnchoice  45386  choicefi  45555  axccdom  45577  dfafn5b  47518  rngchomffvalALTV  48635  ixpv  49246  iinfconstbaslem  49421  iinfconstbas  49422  nelsubc3lem  49426  functhinclem1  49800  cnelsubclem  49959