Theorem feq3 6481

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 3918	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6339	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6339	. 2 ⊢ (𝐹:𝐶⟶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶⟶𝐴 ↔ 𝐹:𝐶⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3858  ran crn 5525   Fn wfn 6330  ⟶wf 6331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339

This theorem is referenced by:  feq23  6482  feq3d  6485  fun2  6526  fconstg  6551  f1eq3  6557  mapvalg  8426  mapsnd  8468  cantnff  9170  axdc4uz  13401  supcvg  15259  lmff  22001  txcn  22326  lmmbr  23958  iscmet3  23993  dvcnvrelem2  24717  itgsubstlem  24747  umgrislfupgr  27015  usgrislfuspgr  27076  wlkv0  27539  isgrpo  28379  vciOLD  28443  isvclem  28459  nmop0h  29873  sitgaddlemb  31834  sitmcl  31837  cvmliftlem15  32776  mtyf  33030  matunitlindflem1  35333  sdclem1  35461  k0004lem1  41223  stoweidlem57  43065  isomushgr  44711