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

Theorem nfab1 2607
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfab1  |-  F/_ x { x  |  ph }

Proof of Theorem nfab1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 nfsab1 2432 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2594 1  |-  F/_ x { x  |  ph }
Colors of variables: wff setvar class
Syntax hints:   {cab 2428   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-13 1985
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-nfc 2593
This theorem is referenced by:  nfabd2  2626  abid2f  2634  abid2fOLD  2635  nfrab1  3024  elabgt  3229  elabgf  3230  nfsbc1d  3331  ss2ab  3553  abn0  3790  euabsn  4087  iunab  4361  iinab  4376  zfrep4  4556  sniota  5568  opabiotafun  5919  nfixp1  7491  scottexs  8308  scott0s  8309  cp  8312  ofpreima  27483  qqhval2  27940  sigaclcu2  28097  compab  31304  ssfiunibd  31458  bnj1366  33621  bnj1321  33816  bnj1384  33821
  Copyright terms: Public domain W3C validator