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

Theorem nfab1 2957
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 2803 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2945 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2799  wnfc 2942
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 2069  ax-7 2105  ax-10 2186  ax-12 2215
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-nfc 2944
This theorem is referenced by:  nfabd2  2975  abid2f  2982  nfrab1  3318  elabgt  3549  elabgf  3550  nfsbc1d  3658  ss2ab  3874  ab0  4159  abn0  4162  euabsn  4459  iunab  4765  iinab  4780  zfrep4  4980  sniota  6094  opabiotafun  6483  nfixp1  8168  scottexs  9000  scott0s  9001  cp  9004  ofpreima  29798  qqhval2  30357  esum2dlem  30485  sigaclcu2  30514  bnj1366  31228  bnj1321  31423  bnj1384  31428  mptsnunlem  33504  topdifinffinlem  33513  compab  39145  ssfiunibd  40005  absnsb  41652  setrec2lem2  43010
  Copyright terms: Public domain W3C validator