Theorem feq3 6648

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502

This theorem is referenced by:  feq23  6649  feq3d  6653  fun2  6703  fconstg  6727  f1eq3  6733  mapvalg  8783  mapsnd  8834  cantnff  9595  axdc4uz  13946  supcvg  15821  lmff  23266  txcn  23591  lmmbr  25225  iscmet3  25260  dvcnvrelem2  25985  itgsubstlem  26015  umgrislfupgr  29192  uspgriedgedg  29245  usgrislfuspgr  29256  wlkv0  29718  isgrpo  30568  vciOLD  30632  isvclem  30648  nmop0h  32062  sitgaddlemb  34492  sitmcl  34495  cvmliftlem15  35480  mtyf  35734  matunitlindflem1  37937  sdclem1  38064  k0004lem1  44574  relpeq5  45375  stoweidlem57  46485  f1ocof1ob  47529  isuspgrim0lem  48369  gricushgr  48393  uspgrlimlem4  48467  mof02  49314  mofsn2  49320  mofeu  49323  fdomne0  49325  f002  49329  fullthinc  49925  functermc  49983