Theorem nfs1v 2157

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2157 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 2086	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2152	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1853	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  hbs1  2274  sb8fOLD  2353  sb8ef  2354  sbbib  2360  sb2ae  2495  mo3  2558  eu1  2604  2mo  2642  2eu6  2651  nfsab1  2716  cbvrexsvw  3294  cbvralsvwOLD  3295  cbvralsvwOLDOLD  3296  cbvrexsvwOLD  3297  cbvralf  3337  cbvralsv  3343  cbvrexsv  3344  cbvrabwOLD  3449  cbvrab  3454  sbhypfOLD  3520  mob2  3694  reu2  3704  reu2eqd  3715  sbcralt  3843  sbcreu  3847  cbvrabcsfw  3911  cbvreucsf  3914  cbvrabcsf  3915  sbcel12  4382  sbceqg  4383  2nreu  4415  csbif  4554  rexreusng  4651  cbvopab1  5189  cbvopab1g  5190  cbvopab1s  5192  cbvmptf  5215  cbvmptfg  5216  csbopab  5523  csbopabgALT  5524  opeliunxp  5713  opeliun2xp  5714  ralxpf  5818  cbviotaw  6479  cbviota  6481  csbiota  6512  isarep1  6614  isarep1OLD  6615  f1ossf1o  7107  cbvriotaw  7360  cbvriota  7364  csbriota  7366  onminex  7785  tfis  7839  findes  7885  abrexex2g  7952  dfoprab4f  8044  axrepndlem1  10563  axrepndlem2  10564  uzind4s  12881  mo5f  32425  ac6sf2  32556  esumcvg  34084  bj-gabima  36925  wl-lem-moexsb  37553  wl-mo3t  37561  poimirlem26  37637  sbcalf  38105  sbcexf  38106  sbcrexgOLD  42745  scottabes  44203  2sb5nd  44522  2sb5ndALT  44893  2reu8i  47084  dfich2  47414