Theorem feq3 6718

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565

This theorem is referenced by:  feq23  6719  feq3d  6723  fun2  6771  fconstg  6795  f1eq3  6801  mapvalg  8876  mapsnd  8926  cantnff  9714  axdc4uz  14025  supcvg  15892  lmff  23309  txcn  23634  lmmbr  25292  iscmet3  25327  dvcnvrelem2  26057  itgsubstlem  26089  umgrislfupgr  29140  uspgriedgedg  29193  usgrislfuspgr  29204  wlkv0  29669  isgrpo  30516  vciOLD  30580  isvclem  30596  nmop0h  32010  sitgaddlemb  34350  sitmcl  34353  cvmliftlem15  35303  mtyf  35557  matunitlindflem1  37623  sdclem1  37750  k0004lem1  44160  relpeq5  44969  stoweidlem57  46072  f1ocof1ob  47093  isuspgrim0lem  47871  gricushgr  47886  uspgrlimlem4  47958  mof02  48748  mofsn2  48754  mofeu  48757  fdomne0  48759  f002  48763  fullthinc  49099  functermc  49140