# 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 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfxp.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfxp ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 nfxp.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfxp.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-xp ${⊢}{A}×{B}=\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}\in {B}\right)\right\}$
4 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
5 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {B}$
6 4 5 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {z}\in {B}\right)$
7 6 nfopab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{⟨{y},{z}⟩|\left({y}\in {A}\wedge {z}\in {B}\right)\right\}$
8 3 7 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}×{B}\right)$