This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Ⅎ 𝑥 ( 𝐴 × 𝐵 )