Theorem nfmpo1 7436

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 7361	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		nfoprab1 7417	. 2 ⊢ Ⅎ𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
3	1, 2	nfcxfr 2899	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Ⅎwnfc 2886  {coprab 7357   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  ovmpos  7504  ov2gf  7505  ovmpodxf  7506  ovmpodf  7512  ovmpodv2  7514  xpcomco  8995  mapxpen  9071  pwfseqlem2  10573  pwfseqlem4a  10575  pwfseqlem4  10576  gsum2d2lem  19939  gsum2d2  19940  gsumcom2  19941  dprd2d2  20012  cnmpt21  23654  cnmpt2t  23656  cnmptcom  23661  cnmpt2k  23671  xkocnv  23797  numclwlk2lem2f1o  30467  finxpreclem2  37752  mnringmulrcld  44672  fmuldfeqlem1  46027  fmuldfeq  46028  ovmpordxf  48830