Theorem feq3 6730

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ⊆ wss 3976  ran crn 5701   Fn wfn 6568  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577

This theorem is referenced by:  feq23  6731  feq3d  6734  fun2  6784  fconstg  6808  f1eq3  6814  mapvalg  8894  mapsnd  8944  cantnff  9743  axdc4uz  14035  supcvg  15904  lmff  23330  txcn  23655  lmmbr  25311  iscmet3  25346  dvcnvrelem2  26077  itgsubstlem  26109  umgrislfupgr  29158  uspgriedgedg  29211  usgrislfuspgr  29222  wlkv0  29687  isgrpo  30529  vciOLD  30593  isvclem  30609  nmop0h  32023  sitgaddlemb  34313  sitmcl  34316  cvmliftlem15  35266  mtyf  35520  matunitlindflem1  37576  sdclem1  37703  k0004lem1  44109  stoweidlem57  45978  f1ocof1ob  46996  isuspgrim0lem  47755  gricushgr  47770  uspgrlimlem4  47815  mof02  48552  mofsn2  48558  mofeu  48561  fdomne0  48563  f002  48567  fullthinc  48713