Theorem nfmpo2 7214

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

Assertion

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

Proof of Theorem nfmpo2

Dummy variable 𝑧 is distinct from all other variables.

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

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Ⅎwnfc 2936  {coprab 7136   ∈ cmpo 7137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-oprab 7139  df-mpo 7140

This theorem is referenced by:  ovmpos  7277  ov2gf  7278  ovmpodxf  7279  ovmpodf  7285  ovmpodv2  7287  xpcomco  8590  mapxpen  8667  pwfseqlem2  10070  pwfseqlem4a  10072  pwfseqlem4  10073  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  dprd2d2  19159  cnmpt21  22276  cnmpt2t  22278  cnmptcom  22283  cnmpt2k  22293  xkocnv  22419  finxpreclem2  34807  finxpreclem6  34813  mnringmulrcld  40936  fmuldfeq  42225  smflimlem6  43409  ovmpordxf  44740