Theorem nfs1v 2154

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1786  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069

This theorem is referenced by:  hbs1  2266  sb5OLD  2269  sb8fOLD  2351  sb8ef  2352  sbbib  2358  sb2ae  2496  mo3  2559  eu1  2607  2mo  2645  2eu6  2653  nfsab1  2718  cbvralsvw  3315  cbvrexsvw  3316  cbvralsvwOLD  3317  cbvrexsvwOLD  3318  cbvralfwOLD  3321  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvrabw  3468  cbvrab  3474  sbhypfOLD  3539  mob2  3710  reu2  3720  reu2eqd  3731  sbcralt  3865  sbcreu  3869  cbvrabcsfw  3936  cbvreucsf  3939  cbvrabcsf  3940  sbcel12  4407  sbceqg  4408  2nreu  4440  csbif  4584  rexreusng  4682  cbvopab1  5222  cbvopab1g  5223  cbvopab1s  5225  cbvmptf  5256  cbvmptfg  5257  csbopab  5554  csbopabgALT  5555  opeliunxp  5741  ralxpf  5844  cbviotaw  6499  cbviota  6502  csbiota  6533  isarep1  6634  isarep1OLD  6635  f1ossf1o  7121  cbvriotaw  7369  cbvriota  7374  csbriota  7376  onminex  7785  tfis  7839  findes  7888  abrexex2g  7946  dfoprab4f  8037  axrepndlem1  10583  axrepndlem2  10584  uzind4s  12888  mo5f  31707  ac6sf2  31827  esumcvg  33022  bj-gabima  35758  wl-lem-moexsb  36371  wl-mo3t  36379  poimirlem26  36452  sbcalf  36920  sbcexf  36921  sbcrexgOLD  41456  scottabes  42934  2sb5nd  43254  2sb5ndALT  43626  2reu8i  45756  dfich2  46061  opeliun2xp  46910