![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfmpt1 | GIF version |
Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |
Ref | Expression |
---|---|
nfmpt1 | ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt 4081 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
2 | nfopab1 4087 | . 2 ⊢ Ⅎ𝑥{〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
3 | 1, 2 | nfcxfr 2329 | 1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 = wceq 1364 ∈ wcel 2160 Ⅎwnfc 2319 {copab 4078 ↦ cmpt 4079 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-opab 4080 df-mpt 4081 |
This theorem is referenced by: nffvmpt1 5545 fvmptss2 5612 fvmptssdm 5621 fvmptdf 5624 mpteqb 5627 fvmptf 5629 ralrnmpt 5679 rexrnmpt 5680 f1ompt 5688 f1mpt 5793 fliftfun 5818 dom2lem 6798 mapxpen 6876 mkvprop 7186 cc3 7297 nfcprod1 11594 cnmpt11 14243 lgseisenlem2 14912 |
Copyright terms: Public domain | W3C validator |