Theorem fneq1 6634

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 6561	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5888	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2738	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6539	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6539	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5659  Fun wfun 6530   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6538  df-fn 6539

This theorem is referenced by:  fneq1d  6636  fneq1i  6640  fn0  6674  feq1  6691  foeq1  6791  f1ocnv  6835  dffn5  6942  mpteqb  7010  fnsnbg  7161  fnsnbOLD  7163  fnprb  7205  fntpb  7206  eufnfv  7226  frrlem1  8290  frrlem13  8302  wfrlem1OLD  8327  wfrlem3OLDa  8330  wfrlem15OLD  8342  tfrlem12  8408  fsetdmprc0  8874  mapval2  8891  elixp2  8920  ixpfn  8922  elixpsn  8956  inf3lem6  9652  ssttrcl  9734  ttrcltr  9735  ttrclss  9739  ttrclselem2  9745  aceq3lem  10139  dfac4  10141  dfacacn  10161  axcc2lem  10455  axcc3  10457  seqof  14082  ccatvalfn  14604  cshword  14814  0csh0  14816  rrgsupp  20666  lmodfopnelem1  20860  elpt  23515  elptr  23516  ptcmplem3  23997  prdsxmslem2  24473  tgjustr  28458  bnj62  34756  bnj976  34813  bnj66  34896  bnj124  34907  bnj607  34952  bnj873  34960  bnj1234  35049  bnj1463  35091  fineqvac  35133  gblacfnacd  35135  eqresfnbd  42250  dssmapf1od  44012  fnchoice  45020  choicefi  45191  axccdom  45213  dfafn5b  47157  rngchomffvalALTV  48220  ixpv  48832  iinfconstbaslem  48999  iinfconstbas  49000  nelsubc3lem  49004  functhinclem1  49297  cnelsubclem  49447