Theorem feq3 6689

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 3964	. . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 ⊆ 𝐴 ↔ ran 𝐹 ⊆ 𝐵))
2	1	anbi2d 642	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐵)))
3		df-f 6544	. 2 ⊢ (𝐹:𝐶⟶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 ⊆ 𝐴))
4		df-f 6544	. 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 3906  ran crn 5664   Fn wfn 6535  ⟶wf 6536

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6544

This theorem is used by:  feq23  6690  feq3d  6694  fun2  6745  fconstg  6769  f1eq3  6775  mapvalg  8835  mapsnd  8886  cantnff  9646  axdc4uz  14034  supcvg  15929  lmff  23488  txcn  23814  lmmbr  25448  iscmet3  25483  dvcnvrelem2  26208  itgsubstlem  26238  umgrislfupgr  29504  uspgriedgedg  29560  usgrislfuspgr  29571  wlkv0  30033  isgrpo  30896  vciOLD  30960  isvclem  30976  nmop0h  32390  sitgaddlemb  34779  sitmcl  34782  cvmliftlem15  35803  mtyf  36057  matunitlindflem1  38300  sdclem1  38427  k0004lem1  44906  relpeq5  45690  stoweidlem57  46804  f1ocof1ob  47851  isuspgrim0lem  48691  gricushgr  48715  uspgrlimlem4  48789  mof02  49650  mofsn2  49656  mofeu  49659  fdomne0  49661  f002  49665  fullthinc  50261  functermc  50319