Theorem fneq1 6138

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 6067	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5477	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2760	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 749	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6050	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6050	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 303	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1630  dom cdm 5264  Fun wfun 6041   Fn wfn 6042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-br 4803  df-opab 4863  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-fun 6049  df-fn 6050

This theorem is referenced by:  fneq1d  6140  fneq1i  6144  fn0  6170  feq1  6185  foeq1  6270  f1ocnv  6308  dffn5  6401  mpteqb  6459  fnsnb  6594  fnprb  6634  fntpb  6635  eufnfv  6652  wfrlem1  7581  wfrlem3a  7584  wfrlem15  7596  tfrlem12  7652  mapval2  8051  elixp2  8076  ixpfn  8078  elixpsn  8111  inf3lem6  8701  aceq3lem  9131  dfac4  9133  dfacacn  9153  axcc2lem  9448  axcc3  9450  seqof  13050  ccatvalfn  13551  cshword  13735  0csh0  13737  lmodfopnelem1  19099  rrgsupp  19491  elpt  21575  elptr  21576  ptcmplem3  22057  prdsxmslem2  22533  bnj62  31093  bnj976  31153  bnj66  31235  bnj124  31246  bnj607  31291  bnj873  31299  bnj1234  31386  bnj1463  31428  frrlem1  32084  dssmapf1od  38815  fnchoice  39685  choicefi  39889  axccdom  39913  dfafn5b  41745  cshword2  41945  rngchomffvalALTV  42503