Theorem fneq1 6640

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 6568	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5903	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2733	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6546	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6546	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540  dom cdm 5676  Fun wfun 6537   Fn wfn 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-fun 6545  df-fn 6546

This theorem is referenced by:  fneq1d  6642  fneq1i  6646  fn0  6681  feq1  6698  foeq1  6801  f1ocnv  6845  dffn5  6950  mpteqb  7017  fnsnb  7166  fnprb  7212  fntpb  7213  eufnfv  7233  frrlem1  8277  frrlem13  8289  wfrlem1OLD  8314  wfrlem3OLDa  8317  wfrlem15OLD  8329  tfrlem12  8395  fsetdmprc0  8855  mapval2  8872  elixp2  8901  ixpfn  8903  elixpsn  8937  inf3lem6  9634  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  aceq3lem  10121  dfac4  10123  dfacacn  10142  axcc2lem  10437  axcc3  10439  seqof  14032  ccatvalfn  14538  cshword  14748  0csh0  14750  lmodfopnelem1  20740  rrgsupp  21196  elpt  23396  elptr  23397  ptcmplem3  23878  prdsxmslem2  24358  tgjustr  28158  bnj62  34195  bnj976  34252  bnj66  34335  bnj124  34346  bnj607  34391  bnj873  34399  bnj1234  34488  bnj1463  34530  fineqvac  34561  fnsnbt  41518  eqresfnbd  41521  dssmapf1od  43235  fnchoice  44176  choicefi  44358  axccdom  44380  dfafn5b  46328  rngchomffvalALTV  47115  functhinclem1  47823