Theorem nfop

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

	Ref	Expression
Hypotheses	nfop.1	|- F/_ x A
	nfop.2	|- F/_ x B
Assertion	nfop	|- F/_ x <. A , B >.

Proof

Step	Hyp	Ref	Expression
1		nfop.1	|- F/_ x A
2		nfop.2	|- F/_ x B
3		dfopif	|- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
4	1	nfel1	|- F/ x A e. _V
5	2	nfel1	|- F/ x B e. _V
6	4 5	nfan	|- F/ x ( A e. _V /\ B e. _V )
7	1	nfsn	|- F/_ x { A }
8	1 2	nfpr	|- F/_ x { A , B }
9	7 8	nfpr	|- F/_ x { { A } , { A , B } }
10		nfcv	|- F/_ x (/)
11	6 9 10	nfif	|- F/_ x if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
12	3 11	nfcxfr	|- F/_ x <. A , B >.