Theorem nfsbc1v 2996

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 2995	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1471  [wsbc 2977

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 2978

This theorem is referenced by:  elrabsf  3016  cbvralcsf  3134  cbvrexcsf  3135  euotd  4272  findes  4620  omsinds  4639  elfvmptrab1  5631  ralrnmpt  5679  rexrnmpt  5680  dfopab2  6215  dfoprab3s  6216  mpoxopoveq  6266  findcard2  6918  findcard2s  6919  ac6sfi  6927  dcfi  7011  indpi  7372  nn0ind-raph  9401  uzind4s  9622  indstr  9625  fzrevral  10137  exfzdc  10272  uzsinds  10475  zsupcllemstep  11981  infssuzex  11985  prmind2  12155  bj-bdfindes  15179  bj-findes  15211