Theorem fneq1 6609

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 5867	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2731	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6514	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6514	. 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 5638  Fun wfun 6505   Fn wfn 6506

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  fneq1d  6611  fneq1i  6615  fn0  6649  feq1  6666  foeq1  6768  f1ocnv  6812  dffn5  6919  mpteqb  6987  fnsnbg  7138  fnsnbOLD  7140  fnprb  7182  fntpb  7183  eufnfv  7203  frrlem1  8265  frrlem13  8277  tfrlem12  8357  fsetdmprc0  8828  mapval2  8845  elixp2  8874  ixpfn  8876  elixpsn  8910  inf3lem6  9586  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  aceq3lem  10073  dfac4  10075  dfacacn  10095  axcc2lem  10389  axcc3  10391  seqof  14024  ccatvalfn  14546  cshword  14756  0csh0  14758  rrgsupp  20610  lmodfopnelem1  20804  elpt  23459  elptr  23460  ptcmplem3  23941  prdsxmslem2  24417  tgjustr  28401  bnj62  34710  bnj976  34767  bnj66  34850  bnj124  34861  bnj607  34906  bnj873  34914  bnj1234  35003  bnj1463  35045  fineqvac  35087  gblacfnacd  35089  eqresfnbd  42220  dssmapf1od  44010  fnchoice  45023  choicefi  45194  axccdom  45216  dfafn5b  47159  rngchomffvalALTV  48263  ixpv  48875  iinfconstbaslem  49051  iinfconstbas  49052  nelsubc3lem  49056  functhinclem1  49430  cnelsubclem  49589