![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fneq2 | GIF version |
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fneq2 | ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2150 | . . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 460 | . 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))) |
3 | df-fn 5134 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
4 | df-fn 5134 | . 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1332 dom cdm 4547 Fun wfun 5125 Fn wfn 5126 |
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 5134 |
This theorem is referenced by: fneq2d 5222 fneq2i 5226 feq2 5264 foeq2 5350 f1o00 5410 eqfnfv2 5527 tfr0dm 6227 tfrlemisucaccv 6230 tfrlemi1 6237 tfrlemi14d 6238 tfrexlem 6239 tfr1onlemsucfn 6245 tfr1onlemsucaccv 6246 tfr1onlembxssdm 6248 tfr1onlembfn 6249 tfr1onlemaccex 6253 tfr1onlemres 6254 ixpeq1 6611 0fz1 9856 |
Copyright terms: Public domain | W3C validator |