Theorem feq3 6682

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 6537	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6537	. 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 5656   Fn wfn 6528  ⟶wf 6529

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 2732

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

This theorem is used by:  feq23  6683  feq3d  6687  fun2  6738  fconstg  6762  f1eq3  6768  mapvalg  8835  mapsnd  8893  cantnff  9653  axdc4uz  14048  supcvg  15945  matunitlindflem1  22901  lmff  23526  txcn  23852  lmmbr  25486  iscmet3  25521  dvcnvrelem2  26245  itgsubstlem  26275  umgrislfupgr  29580  uspgriedgedg  29636  usgrislfuspgr  29647  wlkv0  30109  isgrpo  30978  vciOLD  31042  isvclem  31058  nmop0h  32472  sitgaddlemb  34859  sitmcl  34862  cvmliftlem15  35877  mtyf  36131  sdclem1  38493  k0004lem1  44987  relpeq5  45771  stoweidlem57  46885  f1ocof1ob  47969  isuspgrim0lem  48809  gricushgr  48833  uspgrlimlem4  48907  mof02  49767  mofsn2  49773  mofeu  49776  fdomne0  49778  f002  49782  fullthinc  50376  functermc  50434