Theorem nfmpt21 6888

Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)

Assertion

Ref	Expression
nfmpt21	⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Proof of Theorem nfmpt21

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt2 6819	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		nfoprab1 6870	. 2 ⊢ Ⅎ𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
3	1, 2	nfcxfr 2900	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   ∧ wa 383   = wceq 1632   ∈ wcel 2139  Ⅎwnfc 2889  {coprab 6815   ↦ cmpt2 6816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-oprab 6818  df-mpt2 6819

This theorem is referenced by:  ovmpt2s  6950  ov2gf  6951  ovmpt2dxf  6952  ovmpt2df  6958  ovmpt2dv2  6960  xpcomco  8217  mapxpen  8293  pwfseqlem2  9693  pwfseqlem4a  9695  pwfseqlem4  9696  gsum2d2lem  18592  gsum2d2  18593  gsumcom2  18594  dprd2d2  18663  cnmpt21  21696  cnmpt2t  21698  cnmptcom  21703  cnmpt2k  21713  xkocnv  21839  numclwlk2lem2f1o  27561  numclwlk2lem2f1oOLD  27568  finxpreclem2  33556  cnfinltrel  33570  fmuldfeqlem1  40335  fmuldfeq  40336  ovmpt2rdxf  42645