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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5170 . . 3 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
21anbi1d 458 . 2 (𝐴 = 𝐵 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶)))
3 df-f 5085 . 2 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
4 df-f 5085 . 2 (𝐹:𝐵𝐶 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹𝐶))
52, 3, 43bitr4g 222 1 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1314  wss 3037  ran crn 4500   Fn wfn 5076  wf 5077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-fn 5084  df-f 5085
This theorem is referenced by:  feq23  5216  feq2d  5218  feq2i  5224  f00  5272  f0dom0  5274  f1eq2  5282  fressnfv  5561  tfrcllemsucfn  6204  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllembfn  6208  tfrcllemaccex  6212  tfrcllemres  6213  tfrcldm  6214  tfrcl  6215  mapvalg  6506  map0g  6536  ac6sfi  6745  isomni  6958  ismkv  6977
  Copyright terms: Public domain W3C validator