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

Theorem nfab 2765
 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 2613 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2751 1 𝑥{𝑦𝜑}
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1705  {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-11 2031  ax-12 2044  ax-13 2245 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-nfc 2750 This theorem is referenced by:  nfaba1  2766  nfun  3752  sbcel12  3960  sbceqg  3961  nfpw  4148  nfpr  4208  nfuni  4413  nfint  4456  intab  4477  nfiun  4519  nfiin  4520  nfiu1  4521  nfii1  4522  nfopab  4685  nfopab1  4686  nfopab2  4687  nfdm  5332  eusvobj2  6603  nfoprab1  6664  nfoprab2  6665  nfoprab3  6666  nfoprab  6667  fun11iun  7080  nfwrecs  7361  nfixp  7878  nfixp1  7879  reclem2pr  9821  nfwrd  13279  mreiincl  16184  lss1d  18891  disjabrex  29258  disjabrexf  29259  esumc  29912  bnj900  30734  bnj1014  30765  bnj1123  30789  bnj1307  30826  bnj1398  30837  bnj1444  30846  bnj1445  30847  bnj1446  30848  bnj1447  30849  bnj1467  30857  bnj1518  30867  bnj1519  30868  dfon2lem3  31418  bj-xnex  32728  sdclem1  33198  heibor1  33268  dihglblem5  36094  sbcel12gOLD  38263  ssfiunibd  39010  hoidmvlelem1  40137  nfsetrecs  41747  setrec2lem2  41755  setrec2  41756
 Copyright terms: Public domain W3C validator