Theorem nfsbc1v 3005

Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfsbc1v	|- F/ x [. A / x ]. ph

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem nfsbc1v

Step	Hyp	Ref	Expression
1		nfcv 2336	. 2 |- F/_ x A
2	1	nfsbc1 3004	1 |- F/ x [. A / x ]. ph

Syntax hints:   F/wnf 1471   [.wsbc 2986

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-sbc 2987

This theorem is referenced by:  elrabsf  3025  cbvralcsf  3144  cbvrexcsf  3145  euotd  4284  findes  4636  omsinds  4655  elfvmptrab1  5653  ralrnmpt  5701  rexrnmpt  5702  elovmporab  6120  elovmporab1w  6121  uchoice  6192  dfopab2  6244  dfoprab3s  6245  mpoxopoveq  6295  findcard2  6947  findcard2s  6948  ac6sfi  6956  opabfi  6994  dcfi  7042  indpi  7404  nn0ind-raph  9437  uzind4s  9658  indstr  9661  fzrevral  10174  exfzdc  10310  uzsinds  10518  zsupcllemstep  12085  infssuzex  12089  prmind2  12261  bj-bdfindes  15511  bj-findes  15543