Theorem nfmpo1 7494

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

Assertion

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

Proof of Theorem nfmpo1

Dummy variable 𝑧 is distinct from all other variables.

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2907  {coprab 7415   ∈ cmpo 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-oprab 7418  df-mpo 7419

This theorem is used by:  ovmpos  7562  ov2gf  7563  ovmpodxf  7564  ovmpodf  7570  ovmpodv2  7572  xpcomco  9068  mapxpen  9144  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  gsum2d2lem  20103  gsum2d2  20104  gsumcom2  20105  dprd2d2  20176  cnmpt21  23900  cnmpt2t  23902  cnmptcom  23907  cnmpt2k  23917  xkocnv  24043  numclwlk2lem2f1o  30862  finxpreclem2  38147  mnringmulrcld  45069  fmuldfeqlem1  46415  fmuldfeq  46416  ovmpordxf  49272