Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > funfni | GIF version |
Description: Inference to convert a function and domain antecedent. (Contributed by NM, 22-Apr-2004.) |
Ref | Expression |
---|---|
funfni.1 | ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑) |
Ref | Expression |
---|---|
funfni | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 5293 | . . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | adantr 274 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹) |
3 | fndm 5295 | . . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
4 | 3 | eleq2d 2240 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴)) |
5 | 4 | biimpar 295 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹) |
6 | funfni.1 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑) | |
7 | 2, 5, 6 | syl2anc 409 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2141 dom cdm 4609 Fun wfun 5190 Fn wfn 5191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 df-fn 5199 |
This theorem is referenced by: fneu 5300 fnbrfvb 5535 fvelrnb 5542 fvelimab 5550 fniinfv 5552 fvco2 5563 eqfnfv 5591 fndmdif 5598 fndmin 5600 elpreima 5612 fniniseg 5613 fniniseg2 5615 fnniniseg2 5616 rexsupp 5617 fnopfv 5623 fnfvelrn 5625 rexrn 5630 ralrn 5631 fsn2 5667 fnressn 5679 eufnfv 5723 rexima 5731 ralima 5732 fniunfv 5738 dff13 5744 foeqcnvco 5766 f1eqcocnv 5767 isocnv2 5788 isoini 5794 f1oiso 5802 fnovex 5883 suppssof1 6075 offveqb 6077 1stexg 6143 2ndexg 6144 smoiso 6278 rdgruledefgg 6351 rdgivallem 6357 frectfr 6376 frecrdg 6384 en1 6773 fnfi 6910 ordiso2 7008 cc2lem 7215 slotex 12430 ismgm 12597 plusffvalg 12602 grpidvalg 12613 fn0g 12615 issgrp 12630 ismnddef 12640 ismhm 12671 issubm 12681 0mhm 12690 |
Copyright terms: Public domain | W3C validator |