Theorem nfsbc1v 3048

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

Syntax hints:  Ⅎwnf 1506  [wsbc 3029

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-sbc 3030

This theorem is referenced by:  elrabsf  3068  cbvralcsf  3188  cbvrexcsf  3189  rabsnifsb  3735  euotd  4345  findes  4699  omsinds  4718  elfvmptrab1  5737  ralrnmpt  5785  rexrnmpt  5786  elovmporab  6217  elovmporab1w  6218  uchoice  6295  dfopab2  6347  dfoprab3s  6348  mpoxopoveq  6401  findcard2  7071  findcard2s  7072  ac6sfi  7080  opabfi  7123  dcfi  7171  indpi  7552  nn0ind-raph  9587  uzind4s  9814  indstr  9817  fzrevral  10330  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  uzsinds  10696  prmind2  12682  gropd  15888  grstructd2dom  15889  bj-bdfindes  16480  bj-findes  16512