|   | 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 6563 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 4 | df-fn 6563 | . 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 1539 dom cdm 5684 Fun wfun 6554 Fn wfn 6555 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-fn 6563 | 
| This theorem is referenced by: fneq2d 6661 fneq2i 6665 feq2 6716 foeq2 6816 f1o00 6882 eqfnfv2 7051 frrlem1 8312 frrlem13 8324 wfrlem1OLD 8349 wfrlem15OLD 8364 tfrlem12 8430 ixpeq1 8949 ac5 10518 0fz1 13585 esumcvgsum 34090 bnj90 34737 bnj919 34782 bnj535 34905 bnj1463 35070 fnchoice 45039 | 
| Copyright terms: Public domain | W3C validator |