Theorem feq3 6567

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422

This theorem is referenced by:  feq23  6568  feq3d  6571  fun2  6621  fconstg  6645  f1eq3  6651  mapvalg  8583  mapsnd  8632  cantnff  9362  axdc4uz  13632  supcvg  15496  lmff  22360  txcn  22685  lmmbr  24327  iscmet3  24362  dvcnvrelem2  25087  itgsubstlem  25117  umgrislfupgr  27396  usgrislfuspgr  27457  wlkv0  27920  isgrpo  28760  vciOLD  28824  isvclem  28840  nmop0h  30254  sitgaddlemb  32215  sitmcl  32218  cvmliftlem15  33160  mtyf  33414  matunitlindflem1  35700  sdclem1  35828  k0004lem1  41646  stoweidlem57  43488  f1ocof1ob  44460  isomushgr  45166  mof02  46054  mofsn2  46060  mofeu  46063  fdomne0  46065  f002  46069  fullthinc  46215