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

Theorem nfab 2910
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2371. See nfabg 2911 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 2723 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2887 1 𝑥{𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1786  {cab 2710  wnfc 2884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-11 2155  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-nfc 2886
This theorem is referenced by:  nfaba1  2912  nfun  4126  sbcel12  4369  sbceqg  4370  nfpw  4580  nfpr  4652  nfint  4918  intab  4940  nfiun  4985  nfiin  4986  nfiu1  4989  nfii1  4990  nfopab1  5176  nfopab2  5177  nfdm  5907  eusvobj2  7350  nfoprab1  7419  nfoprab2  7420  nfoprab3  7421  nfoprab  7422  fiun  7876  f1iun  7877  nffrecs  8215  nfwrecsOLD  8249  nfixpw  8857  nfixp  8858  nfixp1  8859  reclem2pr  10989  nfwrd  14437  mreiincl  17481  lss1d  20439  iinabrex  31533  disjabrex  31546  disjabrexf  31547  esumc  32707  bnj900  33598  bnj1014  33630  bnj1123  33655  bnj1307  33692  bnj1398  33703  bnj1444  33712  bnj1445  33713  bnj1446  33714  bnj1447  33715  bnj1467  33723  bnj1518  33733  bnj1519  33734  fineqvrep  33753  dfon2lem3  34416  sdclem1  36248  heibor1  36315  dihglblem5  39807  ssfiunibd  43630  hoidmvlelem1  44922  nfsetrecs  47217  setrec2lem2  47225  setrec2  47226
  Copyright terms: Public domain W3C validator