| 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 2748 | . . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵)) | |
| 2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))) |
| 3 | df-fn 6495 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 4 | df-fn 6495 | . 2 ⊢ (𝐹 Fn 𝐵 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 dom cdm 5624 Fun wfun 6486 Fn wfn 6487 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2728 df-fn 6495 |
| This theorem is referenced by: fneq2d 6586 fneq2i 6590 feq2 6641 foeq2 6743 f1o00 6809 eqfnfv2 6977 frrlem1 8228 frrlem13 8240 tfrlem12 8320 ixpeq1 8846 ac5 10387 0fz1 13460 fconst7v 32698 esumcvgsum 34245 bnj90 34878 bnj919 34923 bnj535 35046 bnj1463 35211 fnchoice 45274 |
| Copyright terms: Public domain | W3C validator |