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

Theorem nfab1 2753
 Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfab1 𝑥{𝑥𝜑}

Proof of Theorem nfab1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 nfsab1 2600 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2741 1 𝑥{𝑥𝜑}
 Colors of variables: wff setvar class Syntax hints:  {cab 2596  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-nfc 2740 This theorem is referenced by:  nfabd2  2770  abid2f  2777  nfrab1  3099  elabgt  3316  elabgf  3317  nfsbc1d  3420  ss2ab  3633  ab0  3905  abn0  3908  euabsn  4205  iunab  4502  iinab  4517  zfrep4  4707  sniota  5795  opabiotafun  6169  nfixp1  7814  scottexs  8633  scott0s  8634  cp  8637  ofpreima  28848  qqhval2  29354  esum2dlem  29481  sigaclcu2  29510  bnj1366  30154  bnj1321  30349  bnj1384  30354  mptsnunlem  32361  topdifinffinlem  32371  compab  37666  ssfiunibd  38464  setrec2lem2  42240
 Copyright terms: Public domain W3C validator