![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fneq2 | Structured version Visualization version 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 2745 | . . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))) |
3 | df-fn 6547 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
4 | df-fn 6547 | . 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 dom cdm 5677 Fun wfun 6538 Fn wfn 6539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-fn 6547 |
This theorem is referenced by: fneq2d 6644 fneq2i 6648 feq2 6700 foeq2 6803 f1o00 6869 eqfnfv2 7034 frrlem1 8271 frrlem13 8283 wfrlem1OLD 8308 wfrlem15OLD 8323 tfrlem12 8389 ixpeq1 8902 ac5 10472 0fz1 13521 esumcvgsum 33086 bnj90 33733 bnj919 33778 bnj535 33901 bnj1463 34066 fnchoice 43713 |
Copyright terms: Public domain | W3C validator |