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

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

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3733 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 742 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6005 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6005 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wss 3680  ran crn 5219   Fn wfn 5996  wf 5997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-in 3687  df-ss 3694  df-f 6005
This theorem is referenced by:  feq23  6142  feq3d  6145  fun2  6180  fconstg  6205  f1eq3  6211  mapvalg  7984  mapsn  8016  cantnff  8684  axdc4uz  12898  supcvg  14708  lmff  21228  txcn  21552  lmmbr  23177  iscmet3  23212  dvcnvrelem2  23901  itgsubstlem  23931  umgrislfupgr  26138  usgrislfuspgr  26199  wlkv0  26678  isgrpo  27581  vciOLD  27646  isvclem  27662  nmop0h  29080  sitgaddlemb  30640  sitmcl  30643  cvmliftlem15  31508  mtyf  31677  matunitlindflem1  33637  sdclem1  33771  k0004lem1  38864  mapsnd  39804  stoweidlem57  40694
  Copyright terms: Public domain W3C validator