![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfrabw | GIF version |
Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by Jim Kingdon, 19-Jul-2018.) |
Ref | Expression |
---|---|
nfrabw.1 | ⊢ Ⅎ𝑥𝜑 |
nfrabw.2 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfrabw | ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 2481 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} | |
2 | nfrabw.2 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2330 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfrabw.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 3, 4 | nfan 1576 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑) |
6 | 5 | nfab 2341 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} |
7 | 1, 6 | nfcxfr 2333 | 1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 Ⅎwnf 1471 ∈ wcel 2164 {cab 2179 Ⅎwnfc 2323 {crab 2476 |
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 2175 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-rab 2481 |
This theorem is referenced by: nfdif 3280 nfin 3365 nfse 4370 elfvmptrab1 5644 elovmporab 6110 elovmporab1w 6111 mpoxopoveq 6284 nfsup 7041 caucvgprprlemaddq 7758 ctiunct 12587 |
Copyright terms: Public domain | W3C validator |