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 5220 | . . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | adantr 274 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹) |
3 | fndm 5222 | . . . 4 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
4 | 3 | eleq2d 2209 | . . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴)) |
5 | 4 | biimpar 295 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ dom 𝐹) |
6 | funfni.1 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → 𝜑) | |
7 | 2, 5, 6 | syl2anc 408 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1480 dom cdm 4539 Fun wfun 5117 Fn wfn 5118 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 df-fn 5126 |
This theorem is referenced by: fneu 5227 fnbrfvb 5462 fvelrnb 5469 fvelimab 5477 fniinfv 5479 fvco2 5490 eqfnfv 5518 fndmdif 5525 fndmin 5527 elpreima 5539 fniniseg 5540 fniniseg2 5542 fnniniseg2 5543 rexsupp 5544 fnopfv 5550 fnfvelrn 5552 rexrn 5557 ralrn 5558 fsn2 5594 fnressn 5606 eufnfv 5648 rexima 5656 ralima 5657 fniunfv 5663 dff13 5669 foeqcnvco 5691 f1eqcocnv 5692 isocnv2 5713 isoini 5719 f1oiso 5727 fnovex 5804 suppssof1 5999 offveqb 6001 1stexg 6065 2ndexg 6066 smoiso 6199 rdgruledefgg 6272 rdgivallem 6278 frectfr 6297 frecrdg 6305 en1 6693 fnfi 6825 ordiso2 6920 slotex 11986 |
Copyright terms: Public domain | W3C validator |