Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 df-rab 3057 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1877 . . . 4 𝑦
3 nfrab.2 . . . . . . . 8 𝑥𝐴
43nfcri 2894 . . . . . . 7 𝑥 𝑧𝐴
5 eleq1w 2820 . . . . . . 7 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
64, 5dvelimnf 2477 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦𝐴)
7 nfrab.1 . . . . . . 7 𝑥𝜑
87a1i 11 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
96, 8nfand 1973 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦𝐴𝜑))
109adantl 473 . . . 4 ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦𝐴𝜑))
112, 10nfabd2 2920 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
1211trud 1640 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
131, 12nfcxfr 2898 1 𝑥{𝑦𝐴𝜑}
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator