Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq3 Structured version   Visualization version   GIF version

Theorem feq3 6481
 Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq3 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3918 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 631 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6339 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6339 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 317 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3858  ran crn 5525   Fn wfn 6330  ⟶wf 6331 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339 This theorem is referenced by:  feq23  6482  feq3d  6485  fun2  6526  fconstg  6551  f1eq3  6557  mapvalg  8426  mapsnd  8468  cantnff  9170  axdc4uz  13401  supcvg  15259  lmff  22001  txcn  22326  lmmbr  23958  iscmet3  23993  dvcnvrelem2  24717  itgsubstlem  24747  umgrislfupgr  27015  usgrislfuspgr  27076  wlkv0  27539  isgrpo  28379  vciOLD  28443  isvclem  28459  nmop0h  29873  sitgaddlemb  31834  sitmcl  31837  cvmliftlem15  32776  mtyf  33030  matunitlindflem1  35333  sdclem1  35461  k0004lem1  41223  stoweidlem57  43065  isomushgr  44711
 Copyright terms: Public domain W3C validator