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 5295 | . . 3 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | adantr 274 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → Fun 𝐹) |
3 | fndm 5297 | . . . 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 4611 Fun wfun 5192 Fn wfn 5193 |
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 5201 |
This theorem is referenced by: fneu 5302 fnbrfvb 5537 fvelrnb 5544 fvelimab 5552 fniinfv 5554 fvco2 5565 eqfnfv 5593 fndmdif 5601 fndmin 5603 elpreima 5615 fniniseg 5616 fniniseg2 5618 fnniniseg2 5619 rexsupp 5620 fnopfv 5626 fnfvelrn 5628 rexrn 5633 ralrn 5634 fsn2 5670 fnressn 5682 eufnfv 5726 rexima 5734 ralima 5735 fniunfv 5741 dff13 5747 foeqcnvco 5769 f1eqcocnv 5770 isocnv2 5791 isoini 5797 f1oiso 5805 fnovex 5886 suppssof1 6078 offveqb 6080 1stexg 6146 2ndexg 6147 smoiso 6281 rdgruledefgg 6354 rdgivallem 6360 frectfr 6379 frecrdg 6387 en1 6777 fnfi 6914 ordiso2 7012 cc2lem 7228 slotex 12443 ismgm 12611 plusffvalg 12616 grpidvalg 12627 fn0g 12629 issgrp 12644 ismnddef 12654 ismhm 12685 issubm 12695 0mhm 12704 grpinvfvalg 12745 grpinvval 12746 grpinvfng 12747 grpsubfvalg 12748 grpsubval 12749 |
Copyright terms: Public domain | W3C validator |