Theorem feq3 6688

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3926  ran crn 5655   Fn wfn 6526  ⟶wf 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6535

This theorem is referenced by:  feq23  6689  feq3d  6693  fun2  6741  fconstg  6765  f1eq3  6771  mapvalg  8850  mapsnd  8900  cantnff  9688  axdc4uz  14002  supcvg  15872  lmff  23239  txcn  23564  lmmbr  25210  iscmet3  25245  dvcnvrelem2  25975  itgsubstlem  26007  umgrislfupgr  29102  uspgriedgedg  29155  usgrislfuspgr  29166  wlkv0  29631  isgrpo  30478  vciOLD  30542  isvclem  30558  nmop0h  31972  sitgaddlemb  34380  sitmcl  34383  cvmliftlem15  35320  mtyf  35574  matunitlindflem1  37640  sdclem1  37767  k0004lem1  44171  relpeq5  44973  stoweidlem57  46086  f1ocof1ob  47110  isuspgrim0lem  47906  gricushgr  47930  uspgrlimlem4  48003  mof02  48817  mofsn2  48823  mofeu  48826  fdomne0  48828  f002  48832  fullthinc  49336  functermc  49393