Theorem feq3 6671

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518

This theorem is referenced by:  feq23  6672  feq3d  6676  fun2  6726  fconstg  6750  f1eq3  6756  mapvalg  8812  mapsnd  8862  cantnff  9634  axdc4uz  13956  supcvg  15829  lmff  23195  txcn  23520  lmmbr  25165  iscmet3  25200  dvcnvrelem2  25930  itgsubstlem  25962  umgrislfupgr  29057  uspgriedgedg  29110  usgrislfuspgr  29121  wlkv0  29586  isgrpo  30433  vciOLD  30497  isvclem  30513  nmop0h  31927  sitgaddlemb  34346  sitmcl  34349  cvmliftlem15  35292  mtyf  35546  matunitlindflem1  37617  sdclem1  37744  k0004lem1  44143  relpeq5  44945  stoweidlem57  46062  f1ocof1ob  47086  isuspgrim0lem  47897  gricushgr  47921  uspgrlimlem4  47994  mof02  48831  mofsn2  48837  mofeu  48840  fdomne0  48842  f002  48846  fullthinc  49443  functermc  49501