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 ⊢ Ⅎ _ x A
nfxp.2 ⊢ Ⅎ _ x B
Assertion nfxp ⊢ Ⅎ _ x A × B

Proof

Step Hyp Ref Expression
1 nfxp.1 ⊢ Ⅎ _ x A
2 nfxp.2 ⊢ Ⅎ _ x B
3 df-xp ⊢ A × B = y z | y ∈ A ∧ z ∈ B
4 1 nfcri ⊢ Ⅎ x y ∈ A
5 2 nfcri ⊢ Ⅎ x z ∈ B
6 4 5 nfan ⊢ Ⅎ x y ∈ A ∧ z ∈ B
7 6 nfopab ⊢ Ⅎ _ x y z | y ∈ A ∧ z ∈ B
8 3 7 nfcxfr ⊢ Ⅎ _ x A × B