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

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

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 4010 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6565 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6565 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wss 3951  ran crn 5686   Fn wfn 6556  wf 6557
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 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565
This theorem is referenced by:  feq23  6719  feq3d  6723  fun2  6771  fconstg  6795  f1eq3  6801  mapvalg  8876  mapsnd  8926  cantnff  9714  axdc4uz  14025  supcvg  15892  lmff  23309  txcn  23634  lmmbr  25292  iscmet3  25327  dvcnvrelem2  26057  itgsubstlem  26089  umgrislfupgr  29140  uspgriedgedg  29193  usgrislfuspgr  29204  wlkv0  29669  isgrpo  30516  vciOLD  30580  isvclem  30596  nmop0h  32010  sitgaddlemb  34350  sitmcl  34353  cvmliftlem15  35303  mtyf  35557  matunitlindflem1  37623  sdclem1  37750  k0004lem1  44160  relpeq5  44969  stoweidlem57  46072  f1ocof1ob  47093  isuspgrim0lem  47871  gricushgr  47886  uspgrlimlem4  47958  mof02  48748  mofsn2  48754  mofeu  48757  fdomne0  48759  f002  48763  fullthinc  49099  functermc  49140
  Copyright terms: Public domain W3C validator