Theorem nfsbc1v 2858

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	|- F/ x [. A / x ]. ph

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2228	. 2 |- F/_ x A
2	1	nfsbc1 2857	1 |- F/ x [. A / x ]. ph

Syntax hints:   F/wnf 1394   [.wsbc 2840

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-sbc 2841

This theorem is referenced by:  elrabsf  2877  cbvralcsf  2990  cbvrexcsf  2991  euotd  4079  findes  4416  omsinds  4433  ralrnmpt  5435  rexrnmpt  5436  dfopab2  5951  dfoprab3s  5952  mpt2xopoveq  5997  findcard2  6595  findcard2s  6596  ac6sfi  6604  indpi  6891  nn0ind-raph  8853  uzind4s  9068  indstr  9071  fzrevral  9507  exfzdc  9639  uzsinds  9836  zsupcllemstep  11206  infssuzex  11210  prmind2  11367  bj-bdfindes  11727  bj-findes  11759