![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfrabw | Structured version Visualization version GIF version |
Description: A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3446 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.) |
Ref | Expression |
---|---|
nfrabw.1 | ⊢ Ⅎ𝑥𝜑 |
nfrabw.2 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfrabw | ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3411 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} | |
2 | nftru 1807 | . . . 4 ⊢ Ⅎ𝑦⊤ | |
3 | nfrabw.2 | . . . . . . 7 ⊢ Ⅎ𝑥𝐴 | |
4 | 3 | nfcri 2895 | . . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
5 | nfrabw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝜑 | |
6 | 4, 5 | nfan 1903 | . . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑) |
7 | 6 | a1i 11 | . . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)) |
8 | 2, 7 | nfabdw 2931 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}) |
9 | 8 | mptru 1549 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} |
10 | 1, 9 | nfcxfr 2906 | 1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 ⊤wtru 1543 Ⅎwnf 1786 ∈ wcel 2107 {cab 2714 Ⅎwnfc 2888 {crab 3410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-rab 3411 |
This theorem is referenced by: nfdif 4090 nfin 4181 nfse 5613 elfvmptrab1w 6979 elovmporab 7604 elovmporab1w 7605 ovmpt3rab1 7616 elovmpt3rab1 7618 mpoxopoveq 8155 nfoi 9457 scottex 9828 elmptrab 23194 iundisjf 31549 nnindf 31757 fedgmullem2 32365 bnj1398 33686 bnj1445 33696 bnj1449 33700 nfwlim 34436 finminlem 34819 poimirlem26 36133 poimirlem27 36134 indexa 36221 nfscott 42593 binomcxplemdvbinom 42707 binomcxplemdvsum 42709 binomcxplemnotnn0 42710 infnsuprnmpt 43552 allbutfiinf 43729 supminfrnmpt 43754 supminfxrrnmpt 43780 fnlimfvre 43989 fnlimabslt 43994 dvnprodlem1 44261 stoweidlem16 44331 stoweidlem31 44346 stoweidlem34 44349 stoweidlem35 44350 stoweidlem48 44363 stoweidlem51 44366 stoweidlem53 44368 stoweidlem54 44369 stoweidlem57 44372 stoweidlem59 44374 fourierdlem31 44453 fourierdlem48 44469 fourierdlem51 44472 etransclem32 44581 ovncvrrp 44879 smflim 45092 smflimmpt 45125 smfsupmpt 45130 smfsupxr 45131 smfinfmpt 45134 smflimsuplem7 45141 |
Copyright terms: Public domain | W3C validator |