Theorem feq3 6687

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3926  ran crn 5655   Fn wfn 6525  ⟶wf 6526

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6534

This theorem is referenced by:  feq23  6688  feq3d  6692  fun2  6740  fconstg  6764  f1eq3  6770  mapvalg  8848  mapsnd  8898  cantnff  9686  axdc4uz  14000  supcvg  15870  lmff  23237  txcn  23562  lmmbr  25208  iscmet3  25243  dvcnvrelem2  25973  itgsubstlem  26005  umgrislfupgr  29048  uspgriedgedg  29101  usgrislfuspgr  29112  wlkv0  29577  isgrpo  30424  vciOLD  30488  isvclem  30504  nmop0h  31918  sitgaddlemb  34326  sitmcl  34329  cvmliftlem15  35266  mtyf  35520  matunitlindflem1  37586  sdclem1  37713  k0004lem1  44118  relpeq5  44921  stoweidlem57  46034  f1ocof1ob  47058  isuspgrim0lem  47854  gricushgr  47878  uspgrlimlem4  47951  mof02  48765  mofsn2  48771  mofeu  48774  fdomne0  48776  f002  48780  fullthinc  49284  functermc  49341