Theorem nfxp

Description: Bound-variable hypothesis builder for Cartesian product. (Contributed by NM, 15-Sep-2003) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nfxp.1	⊢ Ⅎ 𝑥 𝐴
	nfxp.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfxp	⊢ Ⅎ 𝑥 ( 𝐴 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfxp.1	⊢ Ⅎ 𝑥 𝐴
2		nfxp.2	⊢ Ⅎ 𝑥 𝐵
3		df-xp	⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
4	1	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
5	2	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐵
6	4 5	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 )
7	6	nfopab	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
8	3 7	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 × 𝐵 )