Theorem fneq1 6576

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 6505	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5845	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2741	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 638	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6488	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6488	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  dom cdm 5618  Fun wfun 6479   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-fun 6487  df-fn 6488

This theorem is referenced by:  fneq1d  6578  fneq1i  6582  fn0  6616  feq1  6633  foeq1  6735  f1ocnv  6779  dffn5  6885  mpteqb  6955  fnsnbg  7108  fnsnbOLD  7110  fnprb  7152  fntpb  7153  eufnfv  7173  frrlem1  8226  frrlem13  8238  tfrlem12  8318  fsetdmprc0  8792  mapval2  8810  elixp2  8839  ixpfn  8841  elixpsn  8875  inf3lem6  9545  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  aceq3lem  10033  dfac4  10035  dfacacn  10055  axcc2lem  10349  axcc3  10351  seqof  14012  ccatvalfn  14534  cshword  14744  0csh0  14746  rrgsupp  20673  lmodfopnelem1  20888  elpt  23555  elptr  23556  ptcmplem3  24037  prdsxmslem2  24512  tgjustr  28560  esplyind  33759  bnj62  34903  bnj976  34960  bnj66  35042  bnj124  35053  bnj607  35098  bnj873  35106  bnj1234  35195  bnj1463  35237  fineqvac  35297  fineqvnttrclse  35305  gblacfnacd  35330  eqresfnbd  42719  dssmapf1od  44465  fnchoice  45477  choicefi  45646  axccdom  45667  dfafn5b  47624  rngchomffvalALTV  48769  ixpv  49380  iinfconstbaslem  49555  iinfconstbas  49556  nelsubc3lem  49560  functhinclem1  49934  cnelsubclem  50093