Theorem nfs1v 2156

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2156 and hbs1 2274 combined. (Revised by Wolf Lammen, 28-Jul-2022.)

Assertion

Ref	Expression
nfs1v	⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		sb6 2085	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2151	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1852	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1782  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1779  df-nf 1783  df-sb 2065

This theorem is referenced by:  hbs1  2274  sb8fOLD  2357  sb8ef  2358  sbbib  2364  sb2ae  2501  mo3  2564  eu1  2610  2mo  2648  2eu6  2657  nfsab1  2722  cbvrexsvw  3318  cbvralsvwOLD  3319  cbvralsvwOLDOLD  3320  cbvrexsvwOLD  3321  cbvralf  3360  cbvralsv  3366  cbvrexsv  3367  cbvrabwOLD  3475  cbvrab  3480  sbhypfOLD  3548  mob2  3727  reu2  3737  reu2eqd  3748  sbcralt  3884  sbcreu  3888  cbvrabcsfw  3955  cbvreucsf  3958  cbvrabcsf  3959  sbcel12  4420  sbceqg  4421  2nreu  4453  csbif  4591  rexreusng  4687  cbvopab1  5226  cbvopab1g  5227  cbvopab1s  5229  cbvmptf  5260  cbvmptfg  5261  csbopab  5569  csbopabgALT  5570  opeliunxp  5760  ralxpf  5864  cbviotaw  6529  cbviota  6531  csbiota  6562  isarep1  6664  isarep1OLD  6665  f1ossf1o  7155  cbvriotaw  7404  cbvriota  7408  csbriota  7410  onminex  7829  tfis  7883  findes  7930  abrexex2g  7997  dfoprab4f  8089  axrepndlem1  10639  axrepndlem2  10640  uzind4s  12957  mo5f  32532  ac6sf2  32656  esumcvg  34081  bj-gabima  36935  wl-lem-moexsb  37563  wl-mo3t  37571  poimirlem26  37647  sbcalf  38115  sbcexf  38116  sbcrexgOLD  42789  scottabes  44254  2sb5nd  44573  2sb5ndALT  44945  2reu8i  47091  dfich2  47411  opeliun2xp  48216