Theorem feq3 6626

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3897  ran crn 5612   Fn wfn 6471  ⟶wf 6472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6480

This theorem is referenced by:  feq23  6627  feq3d  6631  fun2  6681  fconstg  6705  f1eq3  6711  mapvalg  8755  mapsnd  8805  cantnff  9559  axdc4uz  13886  supcvg  15758  lmff  23211  txcn  23536  lmmbr  25180  iscmet3  25215  dvcnvrelem2  25945  itgsubstlem  25977  umgrislfupgr  29096  uspgriedgedg  29149  usgrislfuspgr  29160  wlkv0  29623  isgrpo  30469  vciOLD  30533  isvclem  30549  nmop0h  31963  sitgaddlemb  34353  sitmcl  34356  cvmliftlem15  35334  mtyf  35588  matunitlindflem1  37656  sdclem1  37783  k0004lem1  44180  relpeq5  44981  stoweidlem57  46095  f1ocof1ob  47112  isuspgrim0lem  47924  gricushgr  47948  uspgrlimlem4  48022  mof02  48870  mofsn2  48876  mofeu  48879  fdomne0  48881  f002  48885  fullthinc  49482  functermc  49540