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

Theorem nfab 2911
Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2377. See nfabg 2912 for a less restrictive version requiring more axioms. (Revised by GG, 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 2727 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2893 1 𝑥{𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1783  {cab 2714  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-nfc 2892
This theorem is referenced by:  nfaba1OLD  2914  nfunOLD  4171  sbcel12  4411  sbceqg  4412  nfpw  4619  nfpr  4692  nfint  4956  intab  4978  nfiun  5023  nfiin  5024  nfiu1OLD  5028  nfii1  5029  nfopab1  5213  nfopab2  5214  nfdm  5962  eusvobj2  7423  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  fiun  7967  f1iun  7968  nffrecs  8308  nfwrecsOLD  8342  nfixpw  8956  nfixp  8957  nfixp1  8958  reclem2pr  11088  nfwrd  14581  mreiincl  17639  lss1d  20961  iinabrex  32582  disjabrex  32595  disjabrexf  32596  esumc  34052  bnj900  34943  bnj1014  34975  bnj1123  35000  bnj1307  35037  bnj1398  35048  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1447  35060  bnj1467  35068  bnj1518  35078  bnj1519  35079  fineqvrep  35109  dfon2lem3  35786  sdclem1  37750  heibor1  37817  dihglblem5  41300  ssfiunibd  45321  hoidmvlelem1  46610  nfsetrecs  49205  setrec2lem2  49213  setrec2  49214
  Copyright terms: Public domain W3C validator