Theorem nfsbc1v 3000

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

Assertion

Ref	Expression
nfsbc1v	⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2332	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 2999	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1471  [wsbc 2981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-sbc 2982

This theorem is referenced by:  elrabsf  3020  cbvralcsf  3139  cbvrexcsf  3140  euotd  4279  findes  4627  omsinds  4646  elfvmptrab1  5640  ralrnmpt  5688  rexrnmpt  5689  elovmporab  6106  elovmporab1w  6107  dfopab2  6229  dfoprab3s  6230  mpoxopoveq  6280  findcard2  6932  findcard2s  6933  ac6sfi  6941  dcfi  7026  indpi  7388  nn0ind-raph  9420  uzind4s  9641  indstr  9644  fzrevral  10157  exfzdc  10293  uzsinds  10501  zsupcllemstep  12056  infssuzex  12060  prmind2  12232  bj-bdfindes  15365  bj-findes  15397