Theorem feq3 6719

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ran crn 5659   Fn wfn 6561  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6570

This theorem is used by:  feq23  6720  feq3d  6724  fun2  6775  fconstg  6799  f1eq3  6805  mapvalg  8894  mapsnd  8952  cantnff  9712  axdc4uz  14167  supcvg  16069  matunitlindflem1  23049  lmff  23674  txcn  24000  lmmbr  25634  iscmet3  25669  dvcnvrelem2  26393  itgsubstlem  26423  umgrislfupgr  29758  uspgriedgedg  29814  usgrislfuspgr  29825  wlkv0  30287  isgrpo  31156  vciOLD  31220  isvclem  31236  nmop0h  32650  sitgaddlemb  35091  sitmcl  35094  cvmliftlem15  36271  mtyf  36525  sdclem1  38943  k0004lem1  45408  relpeq5  46202  stoweidlem57  47340  f1ocof1ob  48424  isuspgrim0lem  49264  gricushgr  49288  uspgrlimlem4  49362  mof02  50281  mofsn2  50287  mofeu  50290  fdomne0  50292  f002  50296  fullthinc  50916  functermc  50974