Theorem feq3 6683

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ⊆ wss 3913  ran crn 5660   Fn wfn 6529  ⟶wf 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6538

This theorem is referenced by:  feq23  6684  feq3d  6688  fun2  6739  fconstg  6763  f1eq3  6769  mapvalg  8829  mapsnd  8880  cantnff  9639  axdc4uz  14016  supcvg  15906  lmff  23423  txcn  23748  lmmbr  25382  iscmet3  25417  dvcnvrelem2  26142  itgsubstlem  26172  umgrislfupgr  29410  uspgriedgedg  29463  usgrislfuspgr  29474  wlkv0  29936  isgrpo  30786  vciOLD  30850  isvclem  30866  nmop0h  32280  sitgaddlemb  34679  sitmcl  34682  cvmliftlem15  35685  mtyf  35939  matunitlindflem1  38150  sdclem1  38277  k0004lem1  44760  relpeq5  45544  stoweidlem57  46658  f1ocof1ob  47702  isuspgrim0lem  48542  gricushgr  48566  uspgrlimlem4  48640  mof02  49497  mofsn2  49503  mofeu  49506  fdomne0  49508  f002  49512  fullthinc  50108  functermc  50166