Theorem nfradd-P6 781

Description: If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the sum term '(𝑡₁ + 𝑡₂)'.

'𝑎' is distinct from all other variables.

Hypotheses

Ref	Expression
nfradd-P6.1	⊢ Ⅎ𝑥 𝑎 = 𝑡₁
nfradd-P6.2	⊢ Ⅎ𝑥 𝑎 = 𝑡₂

Assertion

Ref	Expression
nfradd-P6	⊢ Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂)

Distinct variable groups:   𝑡₁,𝑎   𝑡₂,𝑎   𝑥,𝑎

Proof of Theorem nfradd-P6

Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfrv-P6 686	. . . . . 6 ⊢ Ⅎ𝑥 𝑎 = (𝑏 + 𝑐)
2	1	rcp-NDIMP0addall 207	. . . . 5 ⊢ ((𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂) → Ⅎ𝑥 𝑎 = (𝑏 + 𝑐))
3		nfradd-P6.1	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑎 = 𝑡₁
4	3	nfrterm-P6 779	. . . . . . 7 ⊢ Ⅎ𝑥 𝑏 = 𝑡₁
5		nfradd-P6.2	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑎 = 𝑡₂
6	5	nfrterm-P6 779	. . . . . . 7 ⊢ Ⅎ𝑥 𝑐 = 𝑡₂
7	4, 6	nfrand-P6 690	. . . . . 6 ⊢ Ⅎ𝑥(𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂)
8		subaddd-P5.CL 648	. . . . . . 7 ⊢ ((𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂) → (𝑏 + 𝑐) = (𝑡₁ + 𝑡₂))
9	8	subeqr-P5 635	. . . . . 6 ⊢ ((𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂) → (𝑎 = (𝑏 + 𝑐) ↔ 𝑎 = (𝑡₁ + 𝑡₂)))
10	7, 9	subnfr-P6 755	. . . . 5 ⊢ ((𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂) → (Ⅎ𝑥 𝑎 = (𝑏 + 𝑐) ↔ Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂)))
11	2, 10	bimpf-P4 531	. . . 4 ⊢ ((𝑏 = 𝑡₁ ∧ 𝑐 = 𝑡₂) → Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂))
12	11	rcp-NDIMI2 224	. . 3 ⊢ (𝑏 = 𝑡₁ → (𝑐 = 𝑡₂ → Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂)))
13		axL6ex-P5 625	. . 3 ⊢ ∃𝑏 𝑏 = 𝑡₁
14	12, 13	exiav-P5.SH 616	. 2 ⊢ (𝑐 = 𝑡₂ → Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂))
15		axL6ex-P5 625	. 2 ⊢ ∃𝑐 𝑐 = 𝑡₂
16	14, 15	exiav-P5.SH 616	1 ⊢ Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂)

Syntax hints:  term-obj 1   + term-add 4   = wff-equals 6   → wff-imp 10   ∧ wff-and 132  Ⅎwff-nfree 681

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L9-addl 23  ax-L9-addr 24  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682

This theorem is referenced by:  psubaddv-P6  808