Theorem nfsbc1v 3050

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

Syntax hints:  Ⅎwnf 1508  [wsbc 3031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-sbc 3032

This theorem is referenced by:  elrabsf  3070  cbvralcsf  3190  cbvrexcsf  3191  rabsnifsb  3737  euotd  4347  findes  4701  omsinds  4720  elfvmptrab1  5741  ralrnmpt  5789  rexrnmpt  5790  elovmporab  6221  elovmporab1w  6222  uchoice  6299  dfopab2  6351  dfoprab3s  6352  mpoxopoveq  6405  findcard2  7077  findcard2s  7078  ac6sfi  7086  opabfi  7131  dcfi  7179  indpi  7561  nn0ind-raph  9596  uzind4s  9823  indstr  9826  fzrevral  10339  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  uzsinds  10705  prmind2  12691  gropd  15897  grstructd2dom  15898  bj-bdfindes  16544  bj-findes  16576