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

Theorem nfab 2798
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 2643 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2783 1 𝑥{𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1748  {cab 2637  wnfc 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-nfc 2782
This theorem is referenced by:  nfaba1  2799  nfun  3802  sbcel12  4016  sbceqg  4017  nfpw  4205  nfpr  4264  nfuni  4474  nfint  4518  intab  4539  nfiun  4580  nfiin  4581  nfiu1  4582  nfii1  4583  nfopab  4751  nfopab1  4752  nfopab2  4753  nfdm  5399  eusvobj2  6683  nfoprab1  6746  nfoprab2  6747  nfoprab3  6748  nfoprab  6749  fun11iun  7168  nfwrecs  7454  nfixp  7969  nfixp1  7970  reclem2pr  9908  nfwrd  13365  mreiincl  16303  lss1d  19011  disjabrex  29521  disjabrexf  29522  esumc  30241  bnj900  31125  bnj1014  31156  bnj1123  31180  bnj1307  31217  bnj1398  31228  bnj1444  31237  bnj1445  31238  bnj1446  31239  bnj1447  31240  bnj1467  31248  bnj1518  31258  bnj1519  31259  dfon2lem3  31814  nffrecs  31903  sdclem1  33669  heibor1  33739  dihglblem5  36904  sbcel12gOLD  39071  ssfiunibd  39837  hoidmvlelem1  41130  nfsetrecs  42758  setrec2lem2  42766  setrec2  42767
  Copyright terms: Public domain W3C validator