ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfab1 Unicode version

Theorem nfab1 2350
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 2195 . 2  |-  F/ x  y  e.  { x  |  ph }
21nfci 2338 1  |-  F/_ x { x  |  ph }
Colors of variables: wff set class
Syntax hints:   {cab 2191   F/_wnfc 2335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-nfc 2337
This theorem is referenced by:  abid2f  2374  nfrab1  2686  elabgt  2914  elabgf  2915  nfsbc1d  3015  ss2ab  3261  abn0r  3485  euabsn  3703  iunab  3974  iinab  3989  iotaexab  5250  sniota  5262  nfixp1  6805  elabgft1  15714  elabgf2  15716
  Copyright terms: Public domain W3C validator