![]() |
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 6544 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
4 | df-fn 6544 | . 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 5676 Fun wfun 6535 Fn wfn 6536 |
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 6544 |
This theorem is referenced by: fneq2d 6641 fneq2i 6645 feq2 6697 foeq2 6800 f1o00 6866 eqfnfv2 7031 frrlem1 8268 frrlem13 8280 wfrlem1OLD 8305 wfrlem15OLD 8320 tfrlem12 8386 ixpeq1 8899 ac5 10469 0fz1 13518 esumcvgsum 33075 bnj90 33722 bnj919 33767 bnj535 33890 bnj1463 34055 fnchoice 43699 |
Copyright terms: Public domain | W3C validator |