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

Theorem nfab 2961
 Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2379. See nfabg 2962 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
Hypothesis
Ref Expression
nfab.1 𝑥𝜑
Assertion
Ref Expression
nfab 𝑥{𝑦𝜑}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfab.1 . . 3 𝑥𝜑
21nfsab 2789 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2939 1 𝑥{𝑦𝜑}
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1785  {cab 2776  Ⅎwnfc 2936 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-nfc 2938 This theorem is referenced by:  nfaba1  2963  nfun  4092  sbcel12  4316  sbceqg  4317  nfpw  4518  nfpr  4588  nfint  4849  intab  4869  nfiun  4912  nfiin  4913  nfiu1  4916  nfii1  4917  nfopab  5099  nfopab1  5100  nfopab2  5101  nfdm  5788  eusvobj2  7133  nfoprab1  7199  nfoprab2  7200  nfoprab3  7201  nfoprab  7202  fiun  7633  f1iun  7634  nfwrecs  7939  nfixpw  8470  nfixp  8471  nfixp1  8472  reclem2pr  10466  nfwrd  13893  mreiincl  16866  lss1d  19736  iinabrex  30346  disjabrex  30359  disjabrexf  30360  esumc  31456  bnj900  32347  bnj1014  32379  bnj1123  32404  bnj1307  32441  bnj1398  32452  bnj1444  32461  bnj1445  32462  bnj1446  32463  bnj1447  32464  bnj1467  32472  bnj1518  32482  bnj1519  32483  dfon2lem3  33179  nffrecs  33269  sdclem1  35221  heibor1  35288  dihglblem5  38634  ssfiunibd  42002  hoidmvlelem1  43295  nfsetrecs  45275  setrec2lem2  45283  setrec2  45284
 Copyright terms: Public domain W3C validator