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

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

Proof of Theorem feq3
StepHypRef Expression
1 sseq2 3971 . . 3 (𝐴 = 𝐵 → (ran 𝐹𝐴 ↔ ran 𝐹𝐵))
21anbi2d 630 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵)))
3 df-f 6501 . 2 (𝐹:𝐶𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐴))
4 df-f 6501 . 2 (𝐹:𝐶𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹𝐵))
52, 3, 43bitr4g 314 1 (𝐴 = 𝐵 → (𝐹:𝐶𝐴𝐹:𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wss 3911  ran crn 5635   Fn wfn 6492  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-f 6501
This theorem is referenced by:  feq23  6653  feq3d  6656  fun2  6706  fconstg  6730  f1eq3  6736  mapvalg  8778  mapsnd  8827  cantnff  9615  axdc4uz  13895  supcvg  15746  lmff  22668  txcn  22993  lmmbr  24638  iscmet3  24673  dvcnvrelem2  25398  itgsubstlem  25428  umgrislfupgr  28116  usgrislfuspgr  28177  wlkv0  28641  isgrpo  29481  vciOLD  29545  isvclem  29561  nmop0h  30975  sitgaddlemb  33005  sitmcl  33008  cvmliftlem15  33949  mtyf  34203  matunitlindflem1  36120  sdclem1  36248  k0004lem1  42507  stoweidlem57  44384  f1ocof1ob  45399  isomushgr  46104  mof02  46991  mofsn2  46997  mofeu  47000  fdomne0  47002  f002  47006  fullthinc  47152
  Copyright terms: Public domain W3C validator