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

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

Proof of Theorem nfab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3 𝑥𝜑
21nfsab 2798 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2938 1 𝑥{𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1863  {cab 2792  wnfc 2935
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 2068  ax-7 2104  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-nfc 2937
This theorem is referenced by:  nfaba1  2954  nfun  3968  sbcel12  4180  sbceqg  4181  nfpw  4365  nfpr  4424  nfuni  4636  nfint  4679  intab  4699  nfiun  4740  nfiin  4741  nfiu1  4742  nfii1  4743  nfopab  4912  nfopab1  4913  nfopab2  4914  nfdm  5568  eusvobj2  6863  nfoprab1  6930  nfoprab2  6931  nfoprab3  6932  nfoprab  6933  fun11iun  7352  nfwrecs  7640  nfixp  8160  nfixp1  8161  reclem2pr  10151  nfwrd  13540  mreiincl  16457  lss1d  19166  disjabrex  29719  disjabrexf  29720  esumc  30437  bnj900  31320  bnj1014  31351  bnj1123  31375  bnj1307  31412  bnj1398  31423  bnj1444  31432  bnj1445  31433  bnj1446  31434  bnj1447  31435  bnj1467  31443  bnj1518  31453  bnj1519  31454  dfon2lem3  32008  nffrecs  32097  sdclem1  33848  heibor1  33918  dihglblem5  37076  sbcel12gOLD  39249  ssfiunibd  40001  hoidmvlelem1  41288  nfsetrecs  42998  setrec2lem2  43006  setrec2  43007
  Copyright terms: Public domain W3C validator