Theorem feq3 6687

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 3957	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6541	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6541	. 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 3899  ran crn 5652   Fn wfn 6532  ⟶wf 6533

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6541

This theorem is used by:  feq23  6688  feq3d  6692  fun2  6743  fconstg  6767  f1eq3  6773  mapvalg  8849  mapsnd  8907  cantnff  9668  axdc4uz  14120  supcvg  16018  matunitlindflem1  22987  lmff  23612  txcn  23938  lmmbr  25572  iscmet3  25607  dvcnvrelem2  26331  itgsubstlem  26361  umgrislfupgr  29694  uspgriedgedg  29750  usgrislfuspgr  29761  wlkv0  30223  isgrpo  31092  vciOLD  31156  isvclem  31172  nmop0h  32586  sitgaddlemb  34973  sitmcl  34976  cvmliftlem15  36042  mtyf  36296  sdclem1  38657  k0004lem1  45132  relpeq5  45916  stoweidlem57  47036  f1ocof1ob  48120  isuspgrim0lem  48960  gricushgr  48984  uspgrlimlem4  49058  mof02  49918  mofsn2  49924  mofeu  49927  fdomne0  49929  f002  49933  fullthinc  50527  functermc  50585