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

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

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3996 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 628 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6355 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6355 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 315 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wss 3939  ran crn 5554   Fn wfn 6346  wf 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955  df-f 6355
This theorem is referenced by:  feq23  6494  feq3d  6497  fun2  6537  fconstg  6562  f1eq3  6568  mapvalg  8409  mapsnd  8442  cantnff  9129  axdc4uz  13345  supcvg  15203  lmff  21827  txcn  22152  lmmbr  23778  iscmet3  23813  dvcnvrelem2  24532  itgsubstlem  24562  umgrislfupgr  26824  usgrislfuspgr  26885  wlkv0  27348  isgrpo  28190  vciOLD  28254  isvclem  28270  nmop0h  29684  sitgaddlemb  31494  sitmcl  31497  cvmliftlem15  32431  mtyf  32685  matunitlindflem1  34757  sdclem1  34888  k0004lem1  40364  stoweidlem57  42210  isomushgr  43825
  Copyright terms: Public domain W3C validator