Theorem feq3 6141

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ⊆ wss 3680  ran crn 5219   Fn wfn 5996  ⟶wf 5997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-in 3687  df-ss 3694  df-f 6005

This theorem is referenced by:  feq23  6142  feq3d  6145  fun2  6180  fconstg  6205  f1eq3  6211  mapvalg  7984  mapsn  8016  cantnff  8684  axdc4uz  12898  supcvg  14708  lmff  21228  txcn  21552  lmmbr  23177  iscmet3  23212  dvcnvrelem2  23901  itgsubstlem  23931  umgrislfupgr  26138  usgrislfuspgr  26199  wlkv0  26678  isgrpo  27581  vciOLD  27646  isvclem  27662  nmop0h  29080  sitgaddlemb  30640  sitmcl  30643  cvmliftlem15  31508  mtyf  31677  matunitlindflem1  33637  sdclem1  33771  k0004lem1  38864  mapsnd  39804  stoweidlem57  40694