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 5857	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2731	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6502	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6502	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5631  Fun wfun 6493   Fn wfn 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6501  df-fn 6502

This theorem is referenced by:  fneq1d  6593  fneq1i  6597  fn0  6631  feq1  6648  foeq1  6750  f1ocnv  6794  dffn5  6901  mpteqb  6969  fnsnbg  7120  fnsnbOLD  7122  fnprb  7164  fntpb  7165  eufnfv  7185  frrlem1  8242  frrlem13  8254  tfrlem12  8334  fsetdmprc0  8805  mapval2  8822  elixp2  8851  ixpfn  8853  elixpsn  8887  inf3lem6  9562  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  aceq3lem  10049  dfac4  10051  dfacacn  10071  axcc2lem  10365  axcc3  10367  seqof  14000  ccatvalfn  14522  cshword  14732  0csh0  14734  rrgsupp  20586  lmodfopnelem1  20780  elpt  23435  elptr  23436  ptcmplem3  23917  prdsxmslem2  24393  tgjustr  28377  bnj62  34683  bnj976  34740  bnj66  34823  bnj124  34834  bnj607  34879  bnj873  34887  bnj1234  34976  bnj1463  35018  fineqvac  35060  gblacfnacd  35062  eqresfnbd  42193  dssmapf1od  43983  fnchoice  44996  choicefi  45167  axccdom  45189  dfafn5b  47135  rngchomffvalALTV  48239  ixpv  48851  iinfconstbaslem  49027  iinfconstbas  49028  nelsubc3lem  49032  functhinclem1  49406  cnelsubclem  49565