Theorem fneq1 6639

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534  dom cdm 5672  Fun wfun 6536   Fn wfn 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-fun 6544  df-fn 6545

This theorem is referenced by:  fneq1d  6641  fneq1i  6645  fn0  6680  feq1  6697  foeq1  6801  f1ocnv  6845  dffn5  6951  mpteqb  7018  fnsnb  7169  fnprb  7214  fntpb  7215  eufnfv  7235  frrlem1  8285  frrlem13  8297  wfrlem1OLD  8322  wfrlem3OLDa  8325  wfrlem15OLD  8337  tfrlem12  8403  fsetdmprc0  8865  mapval2  8882  elixp2  8911  ixpfn  8913  elixpsn  8947  inf3lem6  9648  ssttrcl  9730  ttrcltr  9731  ttrclss  9735  ttrclselem2  9741  aceq3lem  10135  dfac4  10137  dfacacn  10156  axcc2lem  10451  axcc3  10453  seqof  14048  ccatvalfn  14555  cshword  14765  0csh0  14767  lmodfopnelem1  20770  rrgsupp  21227  elpt  23463  elptr  23464  ptcmplem3  23945  prdsxmslem2  24425  tgjustr  28265  bnj62  34287  bnj976  34344  bnj66  34427  bnj124  34438  bnj607  34483  bnj873  34491  bnj1234  34580  bnj1463  34622  fineqvac  34653  fnsnbt  41641  eqresfnbd  41643  dssmapf1od  43374  fnchoice  44314  choicefi  44496  axccdom  44518  dfafn5b  46464  rngchomffvalALTV  47263  functhinclem1  47970