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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5221 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 461 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 5136 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 5136 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ⊆ wss 3077  ran crn 4549   Fn wfn 5127  ⟶wf 5128 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-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-fn 5135  df-f 5136 This theorem is referenced by:  feq23  5267  feq2d  5269  feq2i  5275  f00  5323  f0dom0  5325  f1eq2  5333  fressnfv  5616  tfrcllemsucfn  6259  tfrcllemsucaccv  6260  tfrcllembxssdm  6262  tfrcllembfn  6263  tfrcllemaccex  6267  tfrcllemres  6268  tfrcldm  6269  tfrcl  6270  mapvalg  6561  map0g  6591  ac6sfi  6801  isomni  7018  ismkv  7037  iswomni  7049
 Copyright terms: Public domain W3C validator