Theorem nfmpt22 6765

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

Assertion

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

Proof of Theorem nfmpt22

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   ∧ wa 383   = wceq 1523   ∈ wcel 2030  Ⅎwnfc 2780  {coprab 6691   ↦ cmpt2 6692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-oprab 6694  df-mpt2 6695

This theorem is referenced by:  ovmpt2s  6826  ov2gf  6827  ovmpt2dxf  6828  ovmpt2df  6834  ovmpt2dv2  6836  xpcomco  8091  mapxpen  8167  pwfseqlem2  9519  pwfseqlem4a  9521  pwfseqlem4  9522  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  dprd2d2  18489  cnmpt21  21522  cnmpt2t  21524  cnmptcom  21529  cnmpt2k  21539  xkocnv  21665  finxpreclem2  33357  finxpreclem6  33363  fmuldfeq  40133  smflimlem6  41305  ovmpt2rdxf  42442