Theorem nfmpo1 7485

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Ⅎwnfc 2883  {coprab 7404   ∈ cmpo 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-oprab 7407  df-mpo 7408

This theorem is referenced by:  ovmpos  7553  ov2gf  7554  ovmpodxf  7555  ovmpodf  7561  ovmpodv2  7563  xpcomco  9074  mapxpen  9155  pwfseqlem2  10671  pwfseqlem4a  10673  pwfseqlem4  10674  gsum2d2lem  19952  gsum2d2  19953  gsumcom2  19954  dprd2d2  20025  cnmpt21  23607  cnmpt2t  23609  cnmptcom  23614  cnmpt2k  23624  xkocnv  23750  numclwlk2lem2f1o  30306  finxpreclem2  37354  mnringmulrcld  44200  fmuldfeqlem1  45559  fmuldfeq  45560  ovmpordxf  48262