Theorem nfsbc1v 3749

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

Syntax hints:  Ⅎwnf 1785  [wsbc 3729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3730

This theorem is referenced by:  elrabsf  3775  cbvralcsf  3880  reusngf  4619  rexreusng  4624  reuprg0  4647  rmosn  4664  rabsnifsb  4667  euotd  5463  reuop  6253  frpoinsg  6303  elfvmptrab1w  6971  elfvmptrab1  6972  ralrnmptw  7042  ralrnmpt  7044  oprabv  7422  elovmporab  7608  elovmporab1w  7609  elovmporab1  7610  ovmpt3rabdm  7621  elovmpt3rab1  7622  tfisg  7800  tfindes  7809  findes  7846  dfopab2  8000  dfoprab3s  8001  ralxpes  8081  ralxp3es  8084  frpoins3xpg  8085  frpoins3xp3g  8086  mpoxopoveq  8164  findcard2  9094  ac6sfi  9189  indexfi  9265  setinds  9665  frinsg  9670  nn0ind-raph  12624  uzind4s  12853  fzrevral  13561  rabssnn0fi  13943  prmind2  16649  elmptrab  23806  isfildlem  23836  2sqreulem4  27435  gropd  29118  grstructd  29119  rspc2daf  32554  opreu2reuALT  32565  bnj919  34930  bnj1468  35008  bnj110  35020  bnj607  35078  bnj873  35086  bnj849  35087  bnj1388  35195  bnj1489  35218  dfon2lem1  35983  rdgssun  37712  indexa  38072  indexdom  38073  sdclem2  38081  sdclem1  38082  fdc1  38085  alrimii  38458  riotasv2s  39422  sbccomieg  43243  rexrabdioph  43244  rexfrabdioph  43245  aomclem6  43509  pm14.24  44881  or2expropbilem2  47497  or2expropbi  47498  ich2exprop  47947  ichnreuop  47948  ichreuopeq  47949  prproropreud  47985  reupr  47998  reuopreuprim  48002