![]() |
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 2187 | . . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 464 | . 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))) |
3 | df-fn 5221 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
4 | df-fn 5221 | . 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 dom cdm 4628 Fun wfun 5212 Fn wfn 5213 |
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 5221 |
This theorem is referenced by: fneq2d 5309 fneq2i 5313 feq2 5351 foeq2 5437 f1o00 5498 eqfnfv2 5616 tfr0dm 6325 tfrlemisucaccv 6328 tfrlemi1 6335 tfrlemi14d 6336 tfrexlem 6337 tfr1onlemsucfn 6343 tfr1onlemsucaccv 6344 tfr1onlembxssdm 6346 tfr1onlembfn 6347 tfr1onlemaccex 6351 tfr1onlemres 6352 ixpeq1 6711 0fz1 10047 |
Copyright terms: Public domain | W3C validator |