Theorem nfrab 3272

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.)

Hypotheses

Ref	Expression
nfrab.1	⊢ Ⅎ𝑥𝜑
nfrab.2	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfrab	⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Proof of Theorem nfrab

Dummy variable 𝑧 is distinct from all other variables.

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 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

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