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

Theorem nfab 2918
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 2763 . 2 𝑥 𝑧 ∈ {𝑦𝜑}
32nfci 2903 1 𝑥{𝑦𝜑}
Colors of variables: wff setvar class
Syntax hints:  wnf 1856  {cab 2757  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-nfc 2902
This theorem is referenced by:  nfaba1  2919  nfun  3920  sbcel12  4127  sbceqg  4128  nfpw  4311  nfpr  4369  nfuni  4580  nfint  4621  intab  4641  nfiun  4682  nfiin  4683  nfiu1  4684  nfii1  4685  nfopab  4852  nfopab1  4853  nfopab2  4854  nfdm  5503  eusvobj2  6784  nfoprab1  6849  nfoprab2  6850  nfoprab3  6851  nfoprab  6852  fun11iun  7271  nfwrecs  7559  nfixp  8079  nfixp1  8080  reclem2pr  10070  nfwrd  13522  mreiincl  16457  lss1d  19169  disjabrex  29726  disjabrexf  29727  esumc  30446  bnj900  31330  bnj1014  31361  bnj1123  31385  bnj1307  31422  bnj1398  31433  bnj1444  31442  bnj1445  31443  bnj1446  31444  bnj1447  31445  bnj1467  31453  bnj1518  31463  bnj1519  31464  dfon2lem3  32019  nffrecs  32108  sdclem1  33864  heibor1  33934  dihglblem5  37101  sbcel12gOLD  39272  ssfiunibd  40033  hoidmvlelem1  41322  nfsetrecs  42954  setrec2lem2  42962  setrec2  42963
  Copyright terms: Public domain W3C validator