Theorem nfrab 3260

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 3057	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
2		nftru 1877	. . . 4 ⊢ Ⅎ𝑦⊤
3		nfrab.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
4	3	nfcri 2894	. . . . . . 7 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴
5		eleq1w 2820	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
6	4, 5	dvelimnf 2477	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfrab.1	. . . . . . 7 ⊢ Ⅎ𝑥𝜑
8	7	a1i 11	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
9	6, 8	nfand 1973	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
10	9	adantl 473	. . . 4 ⊢ ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜑))
11	2, 10	nfabd2 2920	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)})
12	11	trud 1640	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜑)}
13	1, 12	nfcxfr 2898	1 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝜑}

Syntax hints:  ¬ wn 3   ∧ wa 383  ∀wal 1628  ⊤wtru 1631  Ⅎwnf 1855   ∈ wcel 2137  {cab 2744  Ⅎwnfc 2887  {crab 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057

This theorem is referenced by:  nfdif  3872  nfin  3961  nfse  5239  elfvmptrab1  6465  elovmpt2rab  7043  elovmpt2rab1  7044  ovmpt3rab1  7054  elovmpt3rab1  7056  mpt2xopoveq  7512  nfoi  8582  scottex  8919  elmptrab  21830  iundisjf  29707  nnindf  29872  bnj1398  31407  bnj1445  31417  bnj1449  31421  nfwlim  32071  finminlem  32616  poimirlem26  33746  poimirlem27  33747  indexa  33839  binomcxplemdvbinom  39052  binomcxplemdvsum  39054  binomcxplemnotnn0  39055  infnsuprnmpt  39962  allbutfiinf  40143  supminfrnmpt  40168  supminfxrrnmpt  40197  fnlimfvre  40407  fnlimabslt  40412  dvnprodlem1  40662  stoweidlem16  40734  stoweidlem31  40749  stoweidlem34  40752  stoweidlem35  40753  stoweidlem48  40766  stoweidlem51  40769  stoweidlem53  40771  stoweidlem54  40772  stoweidlem57  40775  stoweidlem59  40777  fourierdlem31  40856  fourierdlem48  40872  fourierdlem51  40875  etransclem32  40984  ovncvrrp  41282  smflim  41489  smflimmpt  41520  smfsupmpt  41525  smfsupxr  41526  smfinfmpt  41529  smflimsuplem7  41536