Theorem fneq1 6607

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 6536	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5875	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2763	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 641	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6519	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6519	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559  dom cdm 5643  Fun wfun 6510   Fn wfn 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-fun 6518  df-fn 6519

This theorem is referenced by:  fneq1d  6609  fneq1i  6613  fn0  6647  feq1  6664  foeq1  6769  f1ocnv  6814  dffn5  6920  mpteqb  6990  fnsnbg  7143  fnsnbOLD  7145  fnprb  7187  fntpb  7188  eufnfv  7208  frrlem1  8261  frrlem13  8273  tfrlem12  8354  fsetdmprc0  8830  mapval2  8848  elixp2  8877  ixpfn  8879  elixpsn  8913  inf3lem6  9582  ssttrcl  9664  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  aceq3lem  10070  dfac4  10072  dfacacn  10092  axcc2lem  10387  axcc3  10389  seqof  14066  ccatvalfn  14588  cshword  14798  0csh0  14800  rrgsupp  20738  lmodfopnelem1  20953  elpt  23620  elptr  23621  ptcmplem3  24102  prdsxmslem2  24577  tgjustr  28631  esplyind  33833  bnj62  34977  bnj976  35034  bnj66  35116  bnj124  35127  bnj607  35172  bnj873  35180  bnj1234  35269  bnj1463  35311  fineqvac  35373  fineqvnttrclse  35381  gblacfnacd  35406  eqresfnbd  42812  dssmapf1od  44558  fnchoice  45570  choicefi  45738  axccdom  45759  dfafn5b  47716  rngchomffvalALTV  48861  ixpv  49472  iinfconstbaslem  49647  iinfconstbas  49648  nelsubc3lem  49652  functhinclem1  50026  cnelsubclem  50185