Theorem nfmpo1 7461

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

Syntax hints:   ∧ wa 398   = wceq 1550   ∈ wcel 2132  Ⅎwnfc 2899  {coprab 7382   ∈ cmpo 7383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-oprab 7385  df-mpo 7386

This theorem is referenced by:  ovmpos  7529  ov2gf  7530  ovmpodxf  7531  ovmpodf  7537  ovmpodv2  7539  xpcomco  9024  mapxpen  9100  pwfseqlem2  10603  pwfseqlem4a  10605  pwfseqlem4  10606  gsum2d2lem  19985  gsum2d2  19986  gsumcom2  19987  dprd2d2  20058  cnmpt21  23700  cnmpt2t  23702  cnmptcom  23707  cnmpt2k  23717  xkocnv  23843  numclwlk2lem2f1o  30516  finxpreclem2  37822  mnringmulrcld  44742  fmuldfeqlem1  46096  fmuldfeq  46097  ovmpordxf  48899