Theorem nfpr

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

	Ref	Expression
Hypotheses	nfpr.1	|- F/_ x A
	nfpr.2	|- F/_ x B
Assertion	nfpr	|- F/_ x { A , B }

Proof

Step	Hyp	Ref	Expression
1		nfpr.1	|- F/_ x A
2		nfpr.2	|- F/_ x B
3		dfpr2	|- { A , B } = { y | ( y = A \/ y = B ) }
4	1	nfeq2	|- F/ x y = A
5	2	nfeq2	|- F/ x y = B
6	4 5	nfor	|- F/ x ( y = A \/ y = B )
7	6	nfab	|- F/_ x { y | ( y = A \/ y = B ) }
8	3 7	nfcxfr	|- F/_ x { A , B }