Theorem nfmpo2 7504

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Ⅎwnfc 2913  {coprab 7424   ∈ cmpo 7425

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-oprab 7427  df-mpo 7428

This theorem is used by:  ovmpos  7571  ov2gf  7572  ovmpodxf  7573  ovmpodf  7579  ovmpodv2  7581  xpcomco  9065  mapxpen  9141  pwfseqlem2  10662  pwfseqlem4a  10664  pwfseqlem4  10665  gsum2d2lem  20074  gsum2d2  20075  gsumcom2  20076  dprd2d2  20147  cnmpt21  23865  cnmpt2t  23867  cnmptcom  23872  cnmpt2k  23882  xkocnv  24008  finxpreclem2  38077  finxpreclem6  38083  mnringmulrcld  44993  fmuldfeq  46340  smflimlem6  47531  ovmpordxf  49160