Theorem fneq1 5893

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 5823	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5246	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2612	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 743	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 5807	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 5807	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 302	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  dom cdm 5038  Fun wfun 5798   Fn wfn 5799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-fun 5806  df-fn 5807

This theorem is referenced by:  fneq1d  5895  fneq1i  5899  fn0  5924  feq1  5939  foeq1  6024  f1ocnv  6062  dffn5  6151  mpteqb  6207  fnsnb  6337  fnprb  6377  fntpb  6378  eufnfv  6395  wfrlem1  7301  wfrlem3a  7304  wfrlem15  7316  tfrlem12  7372  mapval2  7773  elixp2  7798  ixpfn  7800  elixpsn  7833  inf3lem6  8413  aceq3lem  8826  dfac4  8828  dfacacn  8846  axcc2lem  9141  axcc3  9143  seqof  12720  ccatvalfn  13218  cshword  13388  0csh0  13390  lmodfopnelem1  18722  rrgsupp  19112  elpt  21185  elptr  21186  ptcmplem3  21668  prdsxmslem2  22144  bnj62  30040  bnj976  30102  bnj66  30184  bnj124  30195  bnj607  30240  bnj873  30248  bnj1234  30335  bnj1463  30377  frrlem1  31024  dssmapf1od  37335  fnchoice  38211  choicefi  38387  axccdom  38411  dfafn5b  39890  cshword2  40300  rngchomffvalALTV  41787