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

Theorem nfrab 3117
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 2921 . 2 {𝑦𝐴𝜑} = {𝑦 ∣ (𝑦𝐴𝜑)}
2 nftru 1727 . . . 4 𝑦
3 nfrab.2 . . . . . . . 8 𝑥𝐴
43nfcri 2761 . . . . . . 7 𝑥 𝑧𝐴
5 eleq1 2692 . . . . . . 7 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
64, 5dvelimnf 2343 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦𝐴)
7 nfrab.1 . . . . . . 7 𝑥𝜑
87a1i 11 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
96, 8nfand 1828 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑦𝐴𝜑))
109adantl 482 . . . 4 ((⊤ ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦𝐴𝜑))
112, 10nfabd2 2786 . . 3 (⊤ → 𝑥{𝑦 ∣ (𝑦𝐴𝜑)})
1211trud 1490 . 2 𝑥{𝑦 ∣ (𝑦𝐴𝜑)}
131, 12nfcxfr 2765 1 𝑥{𝑦𝐴𝜑}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 384  wal 1478  wtru 1481  wnf 1705  wcel 1992  {cab 2612  wnfc 2754  {crab 2916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921
This theorem is referenced by:  nfdif  3714  nfin  3803  nfse  5054  elfvmptrab1  6262  elovmpt2rab  6834  elovmpt2rab1  6835  ovmpt3rab1  6845  elovmpt3rab1  6847  mpt2xopoveq  7291  nfoi  8364  scottex  8693  elmptrab  21535  iundisjf  29238  nnindf  29398  bnj1398  30802  bnj1445  30812  bnj1449  30816  nfwlim  31461  finminlem  31946  poimirlem26  33053  poimirlem27  33054  indexa  33146  binomcxplemdvbinom  38020  binomcxplemdvsum  38022  binomcxplemnotnn0  38023  infnsuprnmpt  38928  allbutfiinf  39098  fnlimfvre  39297  fnlimabslt  39302  dvnprodlem1  39454  stoweidlem16  39527  stoweidlem31  39542  stoweidlem34  39545  stoweidlem35  39546  stoweidlem48  39559  stoweidlem51  39562  stoweidlem53  39564  stoweidlem54  39565  stoweidlem57  39568  stoweidlem59  39570  fourierdlem31  39649  fourierdlem48  39665  fourierdlem51  39668  etransclem32  39777  ovncvrrp  40072  smflim  40279  smflimmpt  40310  smfsupmpt  40315  smfsupxr  40316  smfinfmpt  40319  smflimsuplem7  40326
  Copyright terms: Public domain W3C validator