Theorem feq3 6668

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515

This theorem is referenced by:  feq23  6669  feq3d  6673  fun2  6723  fconstg  6747  f1eq3  6753  mapvalg  8809  mapsnd  8859  cantnff  9627  axdc4uz  13949  supcvg  15822  lmff  23188  txcn  23513  lmmbr  25158  iscmet3  25193  dvcnvrelem2  25923  itgsubstlem  25955  umgrislfupgr  29050  uspgriedgedg  29103  usgrislfuspgr  29114  wlkv0  29579  isgrpo  30426  vciOLD  30490  isvclem  30506  nmop0h  31920  sitgaddlemb  34339  sitmcl  34342  cvmliftlem15  35285  mtyf  35539  matunitlindflem1  37610  sdclem1  37737  k0004lem1  44136  relpeq5  44938  stoweidlem57  46055  f1ocof1ob  47082  isuspgrim0lem  47893  gricushgr  47917  uspgrlimlem4  47990  mof02  48827  mofsn2  48833  mofeu  48836  fdomne0  48838  f002  48842  fullthinc  49439  functermc  49497