Theorem nfsbc1v 3061

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 2384	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfsbc1 3060	1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1509  [wsbc 3042

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-sbc 3043

This theorem is referenced by:  elrabsf  3081  cbvralcsf  3201  cbvrexcsf  3202  rabsnifsb  3757  euotd  4371  findes  4725  omsinds  4744  elfvmptrab1  5772  ralrnmpt  5819  rexrnmpt  5820  elovmporab  6254  elovmporab1w  6255  uchoice  6331  dfopab2  6383  dfoprab3s  6384  mpoxopoveq  6471  findcard2  7146  findcard2s  7147  ac6sfi  7155  opabfi  7200  dcfi  7268  indpi  7657  nn0ind-raph  9695  uzind4s  9922  indstr  9925  fzrevral  10439  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  uzsinds  10806  prmind2  12817  gropd  16042  grstructd2dom  16043  bj-bdfindes  16719  bj-findes  16751