Theorem nfop

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

	Ref	Expression
Hypotheses	nfop.1	⊢ Ⅎ 𝑥 𝐴
	nfop.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfop	⊢ Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩

Proof

Step	Hyp	Ref	Expression
1		nfop.1	⊢ Ⅎ 𝑥 𝐴
2		nfop.2	⊢ Ⅎ 𝑥 𝐵
3		dfopif	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
4	1	nfel1	⊢ Ⅎ 𝑥 𝐴 ∈ V
5	2	nfel1	⊢ Ⅎ 𝑥 𝐵 ∈ V
6	4 5	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
7	1	nfsn	⊢ Ⅎ 𝑥 { 𝐴 }
8	1 2	nfpr	⊢ Ⅎ 𝑥 { 𝐴 , 𝐵 }
9	7 8	nfpr	⊢ Ⅎ 𝑥 { { 𝐴 } , { 𝐴 , 𝐵 } }
10		nfcv	⊢ Ⅎ 𝑥 ∅
11	6 9 10	nfif	⊢ Ⅎ 𝑥 if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
12	3 11	nfcxfr	⊢ Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩