MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxp Structured version   Visualization version   GIF version

Theorem nfxp 5340
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.
StepHypRef Expression
1 df-xp 5314 . 2 (𝐴 × 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
2 nfxp.1 . . . . 5 𝑥𝐴
32nfcri 2941 . . . 4 𝑥 𝑦𝐴
4 nfxp.2 . . . . 5 𝑥𝐵
54nfcri 2941 . . . 4 𝑥 𝑧𝐵
63, 5nfan 1993 . . 3 𝑥(𝑦𝐴𝑧𝐵)
76nfopab 4908 . 2 𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧𝐵)}
81, 7nfcxfr 2945 1 𝑥(𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 384  wcel 2158  wnfc 2934  {copab 4902   × cxp 5306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-opab 4903  df-xp 5314
This theorem is referenced by:  opeliunxp  5367  nfres  5596  mpt2mptsx  7463  dmmpt2ssx  7465  fmpt2x  7466  ovmptss  7489  nfdju  9014  axcc2  9541  fsum2dlem  14720  fsumcom2  14724  fprod2dlem  14927  fprodcom2  14931  gsumcom2  18571  prdsdsf  22381  prdsxmet  22383  aciunf1lem  29786  esum2dlem  30476  poimirlem16  33735  poimirlem19  33738  dvnprodlem1  40638  stoweidlem21  40714  stoweidlem47  40740  opeliun2xp  42676  dmmpt2ssx2  42680
  Copyright terms: Public domain W3C validator