Theorem nfsbc1v 3758

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

Syntax hints:  Ⅎwnf 1784  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-sbc 3739

This theorem is referenced by:  elrabsf  3784  cbvralcsf  3889  reusngf  4628  rexreusng  4633  reuprg0  4656  rmosn  4673  rabsnifsb  4676  euotd  5458  reuop  6248  frpoinsg  6298  elfvmptrab1w  6965  elfvmptrab1  6966  ralrnmptw  7036  ralrnmpt  7038  oprabv  7415  elovmporab  7601  elovmporab1w  7602  elovmporab1  7603  ovmpt3rabdm  7614  elovmpt3rab1  7615  tfisg  7793  tfindes  7802  findes  7839  dfopab2  7993  dfoprab3s  7994  ralxpes  8075  ralxp3es  8078  frpoins3xpg  8079  frpoins3xp3g  8080  mpoxopoveq  8158  findcard2  9084  ac6sfi  9178  indexfi  9254  setinds  9649  frinsg  9654  nn0ind-raph  12583  uzind4s  12816  fzrevral  13522  rabssnn0fi  13903  prmind2  16606  elmptrab  23752  isfildlem  23782  2sqreulem4  27402  gropd  29020  grstructd  29021  rspc2daf  32456  opreu2reuALT  32467  bnj919  34790  bnj1468  34869  bnj110  34881  bnj607  34939  bnj873  34947  bnj849  34948  bnj1388  35056  bnj1489  35079  dfon2lem1  35836  rdgssun  37433  indexa  37783  indexdom  37784  sdclem2  37792  sdclem1  37793  fdc1  37796  alrimii  38169  riotasv2s  39067  sbccomieg  42900  rexrabdioph  42901  rexfrabdioph  42902  aomclem6  43166  pm14.24  44539  or2expropbilem2  47147  or2expropbi  47148  ich2exprop  47585  ichnreuop  47586  ichreuopeq  47587  prproropreud  47623  reupr  47636  reuopreuprim  47640