| 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 3478 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2377. (Revised by GG, 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 3437 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} | |
| 2 | nftru 1804 | . . . 4 ⊢ Ⅎ𝑦⊤ | |
| 3 | nfrabw.2 | . . . . . . 7 ⊢ Ⅎ𝑥𝐴 | |
| 4 | 3 | nfcri 2897 | . . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 5 | nfrabw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝜑 | |
| 6 | 4, 5 | nfan 1899 | . . . . 5 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑) |
| 7 | 6 | a1i 11 | . . . 4 ⊢ (⊤ → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)) |
| 8 | 2, 7 | nfabdw 2927 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}) |
| 9 | 8 | mptru 1547 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} |
| 10 | 1, 9 | nfcxfr 2903 | 1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ⊤wtru 1541 Ⅎwnf 1783 ∈ wcel 2108 {cab 2714 Ⅎwnfc 2890 {crab 3436 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 |
| This theorem is referenced by: nfdifOLD 4130 nfinOLD 4225 nfse 5659 elfvmptrab1w 7043 elovmporab 7679 elovmporab1w 7680 ovmpt3rab1 7691 elovmpt3rab1 7693 mpoxopoveq 8244 nfoi 9554 scottex 9925 elmptrab 23835 iundisjf 32602 nnindf 32821 fedgmullem2 33681 bnj1398 35048 bnj1445 35058 bnj1449 35062 nfwlim 35823 finminlem 36319 poimirlem26 37653 poimirlem27 37654 indexa 37740 nfscott 44258 binomcxplemdvbinom 44372 binomcxplemdvsum 44374 binomcxplemnotnn0 44375 infnsuprnmpt 45257 allbutfiinf 45431 supminfrnmpt 45456 supminfxrrnmpt 45482 fnlimfvre 45689 fnlimabslt 45694 dvnprodlem1 45961 stoweidlem16 46031 stoweidlem31 46046 stoweidlem34 46049 stoweidlem35 46050 stoweidlem48 46063 stoweidlem51 46066 stoweidlem53 46068 stoweidlem54 46069 stoweidlem57 46072 stoweidlem59 46074 fourierdlem31 46153 fourierdlem48 46169 fourierdlem51 46172 etransclem32 46281 ovncvrrp 46579 smflim 46792 smflimmpt 46825 smfsupmpt 46830 smfsupxr 46831 smfinfmpt 46834 smflimsuplem7 46841 |
| Copyright terms: Public domain | W3C validator |