Theorem nfxp 5696

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

Hypotheses

Ref	Expression
nfxp.1	⊢ Ⅎ𝑥𝐴
nfxp.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfxp	⊢ Ⅎ𝑥(𝐴 × 𝐵)

Proof of Theorem nfxp

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:   ∧ wa 401   ∈ wcel 2146  Ⅎwnfc 2912  {copab 5175   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-opab 5176  df-xp 5669

This theorem is used by:  opeliunxp  5730  opeliun2xp  5731  nfres  5982  mpomptsx  8067  dmmpossx  8069  fmpox  8070  ovmptss  8094  nfdju  9909  axcc2  10436  fsum2dlem  15844  fsumcom2  15848  fprod2dlem  16057  fprodcom2  16061  gsumcom2  20089  prdsdsf  24575  prdsxmet  24577  iunxpssiun1  32984  djussxp2  33064  aciunf1lem  33078  gsumpart  33447  esum2dlem  34546  poimirlem16  38344  poimirlem19  38347  dvnprodlem1  46718  stoweidlem21  46793  stoweidlem47  46819  dmmpossx2  49174