Theorem feq3 6692

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq3	⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

Proof of Theorem feq3

Step	Hyp	Ref	Expression
1		sseq2 3935	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6545	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6545	. 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3896  ran crn 5651   Fn wfn 6536  ⟶wf 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897  df-f 6545

This theorem is used by:  feq23  6693  feq3d  6697  fun2  6748  fconstg  6772  f1eq3  6778  mapvalg  8861  mapsnd  8919  cantnff  9680  axdc4uz  14132  supcvg  16032  matunitlindflem1  23001  lmff  23626  txcn  23952  lmmbr  25586  iscmet3  25621  dvcnvrelem2  26345  itgsubstlem  26375  umgrislfupgr  29708  uspgriedgedg  29764  usgrislfuspgr  29775  wlkv0  30237  isgrpo  31106  vciOLD  31170  isvclem  31186  nmop0h  32600  sitgaddlemb  35028  sitmcl  35031  cvmliftlem15  36151  mtyf  36405  sdclem1  38784  k0004lem1  45254  relpeq5  46045  stoweidlem57  47174  f1ocof1ob  48258  isuspgrim0lem  49098  gricushgr  49122  uspgrlimlem4  49196  mof02  50057  mofsn2  50063  mofeu  50066  fdomne0  50068  f002  50072  fullthinc  50692  functermc  50750