Theorem feq3 6666

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ⊆ wss 3902  ran crn 5644   Fn wfn 6511  ⟶wf 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919  df-f 6520

This theorem is referenced by:  feq23  6667  feq3d  6671  fun2  6722  fconstg  6746  f1eq3  6752  mapvalg  8811  mapsnd  8862  cantnff  9623  axdc4uz  13991  supcvg  15877  lmff  23349  txcn  23674  lmmbr  25308  iscmet3  25343  dvcnvrelem2  26068  itgsubstlem  26098  umgrislfupgr  29281  uspgriedgedg  29334  usgrislfuspgr  29345  wlkv0  29807  isgrpo  30657  vciOLD  30721  isvclem  30737  nmop0h  32151  sitgaddlemb  34606  sitmcl  34609  cvmliftlem15  35609  mtyf  35863  matunitlindflem1  38076  sdclem1  38203  k0004lem1  44684  relpeq5  45485  stoweidlem57  46592  f1ocof1ob  47636  isuspgrim0lem  48476  gricushgr  48500  uspgrlimlem4  48574  mof02  49421  mofsn2  49427  mofeu  49430  fdomne0  49432  f002  49436  fullthinc  50032  functermc  50090