Theorem nfxp 5714

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 5687	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
2		nfxp.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2882	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfxp.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2882	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
6	3, 5	nfan 1894	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)
7	6	nfopab 5221	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝐴 × 𝐵)

Syntax hints:   ∧ wa 394   ∈ wcel 2098  Ⅎwnfc 2875  {copab 5214   × cxp 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-opab 5215  df-xp 5687

This theorem is referenced by:  opeliunxp  5748  nfres  5990  mpomptsx  8077  dmmpossx  8079  fmpox  8080  ovmptss  8106  nfdju  9946  axcc2  10476  fsum2dlem  15769  fsumcom2  15773  fprod2dlem  15977  fprodcom2  15981  gsumcom2  19968  prdsdsf  24356  prdsxmet  24358  djussxp2  32556  aciunf1lem  32570  gsumpart  32901  esum2dlem  33881  poimirlem16  37285  poimirlem19  37288  dvnprodlem1  45504  stoweidlem21  45579  stoweidlem47  45605  opeliun2xp  47648  dmmpossx2  47652