ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  feq1 GIF version

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

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 5284 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 4836 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3176 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 470 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 5200 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 5200 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 222 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1348  wss 3121  ran crn 4610   Fn wfn 5191  wf 5192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988  df-opab 4049  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-fun 5198  df-fn 5199  df-f 5200
This theorem is referenced by:  feq1d  5332  feq1i  5338  f00  5387  f0bi  5388  f0dom0  5389  fconstg  5392  f1eq1  5396  fconst2g  5708  tfrcllemsucfn  6329  tfrcllemsucaccv  6330  tfrcllembxssdm  6332  tfrcllembfn  6333  tfrcllemex  6336  tfrcllemaccex  6337  tfrcllemres  6338  tfrcl  6340  elmapg  6635  ac6sfi  6872  updjud  7055  finomni  7112  exmidomni  7114  mkvprop  7130  1fv  10082  upxp  13025  txcn  13028  dceqnconst  14051  dcapnconst  14052
  Copyright terms: Public domain W3C validator