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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5300 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 465 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 5215 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 5215 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 223 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wss 3129  ran crn 4623   Fn wfn 5206  wf 5207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5214  df-f 5215
This theorem is referenced by:  feq23  5346  feq2d  5348  feq2i  5354  f00  5402  f0dom0  5404  f1eq2  5412  fressnfv  5698  tfrcllemsucfn  6347  tfrcllemsucaccv  6348  tfrcllembxssdm  6350  tfrcllembfn  6351  tfrcllemaccex  6355  tfrcllemres  6356  tfrcldm  6357  tfrcl  6358  mapvalg  6651  map0g  6681  ac6sfi  6891  isomni  7127  ismkv  7144  iswomni  7156
  Copyright terms: Public domain W3C validator