![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfrab | Structured version Visualization version GIF version |
Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Ref | Expression |
---|---|
nfrab.1 | ⊢ Ⅎ𝑥𝜑 |
nfrab.2 | ⊢ Ⅎ𝑥𝐴 |
Ref | Expression |
---|---|
nfrab | ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3070 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} | |
2 | nftru 1878 | . . . 4 ⊢ Ⅎ𝑦⊤ | |
3 | nfrab.2 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐴 | |
4 | 3 | nfcri 2907 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
5 | eleq1w 2833 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
6 | 4, 5 | dvelimnf 2489 | . . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
7 | nfrab.1 | . . . . . . 7 ⊢ Ⅎ𝑥𝜑 | |
8 | 7 | a1i 11 | . . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑) |
9 | 6, 8 | nfand 1978 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)) |
10 | 9 | adantl 467 | . . . 4 ⊢ ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑)) |
11 | 2, 10 | nfabd2 2933 | . . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}) |
12 | 11 | trud 1641 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)} |
13 | 1, 12 | nfcxfr 2911 | 1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑} |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 382 ∀wal 1629 ⊤wtru 1632 Ⅎwnf 1856 ∈ wcel 2145 {cab 2757 Ⅎwnfc 2900 {crab 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 |
This theorem is referenced by: nfdif 3882 nfin 3969 nfse 5224 elfvmptrab1 6447 elovmpt2rab 7027 elovmpt2rab1 7028 ovmpt3rab1 7038 elovmpt3rab1 7040 mpt2xopoveq 7497 nfoi 8575 scottex 8912 elmptrab 21851 iundisjf 29740 nnindf 29905 bnj1398 31440 bnj1445 31450 bnj1449 31454 nfwlim 32104 finminlem 32649 poimirlem26 33768 poimirlem27 33769 indexa 33860 binomcxplemdvbinom 39078 binomcxplemdvsum 39080 binomcxplemnotnn0 39081 infnsuprnmpt 39983 allbutfiinf 40163 supminfrnmpt 40188 supminfxrrnmpt 40217 fnlimfvre 40424 fnlimabslt 40429 dvnprodlem1 40679 stoweidlem16 40750 stoweidlem31 40765 stoweidlem34 40768 stoweidlem35 40769 stoweidlem48 40782 stoweidlem51 40785 stoweidlem53 40787 stoweidlem54 40788 stoweidlem57 40791 stoweidlem59 40793 fourierdlem31 40872 fourierdlem48 40888 fourierdlem51 40891 etransclem32 41000 ovncvrrp 41298 smflim 41505 smflimmpt 41536 smfsupmpt 41541 smfsupxr 41542 smfinfmpt 41545 smflimsuplem7 41552 |
Copyright terms: Public domain | W3C validator |