Theorem feq3 6685

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ⊆ wss 3905  ran crn 5662   Fn wfn 6531  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922  df-f 6540

This theorem is referenced by:  feq23  6686  feq3d  6690  fun2  6741  fconstg  6765  f1eq3  6771  mapvalg  8829  mapsnd  8880  cantnff  9639  axdc4uz  14016  supcvg  15906  lmff  23458  txcn  23783  lmmbr  25417  iscmet3  25452  dvcnvrelem2  26177  itgsubstlem  26207  umgrislfupgr  29473  uspgriedgedg  29526  usgrislfuspgr  29537  wlkv0  29999  isgrpo  30849  vciOLD  30913  isvclem  30929  nmop0h  32343  sitgaddlemb  34738  sitmcl  34741  cvmliftlem15  35790  mtyf  36044  matunitlindflem1  38267  sdclem1  38394  k0004lem1  44873  relpeq5  45657  stoweidlem57  46771  f1ocof1ob  47818  isuspgrim0lem  48658  gricushgr  48682  uspgrlimlem4  48756  mof02  49617  mofsn2  49623  mofeu  49626  fdomne0  49628  f002  49632  fullthinc  50228  functermc  50286