Theorem nfpr

Description: Bound-variable hypothesis builder for unordered pairs. (Contributed by NM, 14-Nov-1995)

	Ref	Expression
Hypotheses	nfpr.1	⊢ Ⅎ 𝑥 𝐴
	nfpr.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfpr	⊢ Ⅎ 𝑥 { 𝐴 , 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		nfpr.1	⊢ Ⅎ 𝑥 𝐴
2		nfpr.2	⊢ Ⅎ 𝑥 𝐵
3		dfpr2	⊢ { 𝐴 , 𝐵 } = { 𝑦 ∣ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) }
4	1	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
5	2	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐵
6	4 5	nfor	⊢ Ⅎ 𝑥 ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 )
7	6	nfab	⊢ Ⅎ 𝑥 { 𝑦 ∣ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) }
8	3 7	nfcxfr	⊢ Ⅎ 𝑥 { 𝐴 , 𝐵 }