| 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 2743 | . . 3 ⊢ (𝐴 = 𝐵 → (dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵)) | |
| 2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐵))) |
| 3 | df-fn 6490 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 4 | df-fn 6490 | . 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 5619 Fun wfun 6481 Fn wfn 6482 |
| 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 2121 ax-ext 2703 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2723 df-fn 6490 |
| This theorem is referenced by: fneq2d 6581 fneq2i 6585 feq2 6636 foeq2 6738 f1o00 6804 eqfnfv2 6971 frrlem1 8222 frrlem13 8234 tfrlem12 8314 ixpeq1 8838 ac5 10374 0fz1 13450 fconst7v 32610 esumcvgsum 34108 bnj90 34741 bnj919 34786 bnj535 34909 bnj1463 35074 fnchoice 45131 |
| Copyright terms: Public domain | W3C validator |