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  4269  findes  4617  omsinds  4636  elfvmptrab1  5627  ralrnmpt  5675  rexrnmpt  5676  dfopab2  6209  dfoprab3s  6210  mpoxopoveq  6260  findcard2  6908  findcard2s  6909  ac6sfi  6917  dcfi  7000  indpi  7361  nn0ind-raph  9390  uzind4s  9610  indstr  9613  fzrevral  10125  exfzdc  10260  uzsinds  10462  zsupcllemstep  11966  infssuzex  11970  prmind2  12140  bj-bdfindes  15105  bj-findes  15137