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

Theorem nfaba1 2954
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
Assertion
Ref Expression
nfaba1 𝑥{𝑦 ∣ ∀𝑥𝜑}

Proof of Theorem nfaba1
StepHypRef Expression
1 nfa1 2195 . 2 𝑥𝑥𝜑
21nfab 2953 1 𝑥{𝑦 ∣ ∀𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  wal 1635  {cab 2792  wnfc 2935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-nfc 2937
This theorem is referenced by:  nfopd  4612  nfimad  5685  nfiota1  6062  nffvd  6416  nfunidALT2  34744  nfunidALT  34745  nfopdALT  34746  setrec1  43000
  Copyright terms: Public domain W3C validator