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

Theorem nfab1 2763
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 2611 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2751 1 𝑥{𝑥𝜑}
Colors of variables: wff setvar class
Syntax hints:  {cab 2607  wnfc 2748
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 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-nfc 2750
This theorem is referenced by:  nfabd2  2780  abid2f  2787  nfrab1  3111  elabgt  3330  elabgf  3331  nfsbc1d  3435  ss2ab  3649  ab0  3925  abn0  3928  euabsn  4231  iunab  4532  iinab  4547  zfrep4  4739  sniota  5837  opabiotafun  6216  nfixp1  7872  scottexs  8694  scott0s  8695  cp  8698  ofpreima  29308  qqhval2  29808  esum2dlem  29935  sigaclcu2  29964  bnj1366  30608  bnj1321  30803  bnj1384  30808  mptsnunlem  32817  topdifinffinlem  32827  compab  38127  ssfiunibd  38987  setrec2lem2  41734
  Copyright terms: Public domain W3C validator