Theorem nfmpo2 7502

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Ⅎwnfc 2907  {coprab 7422   ∈ cmpo 7423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-oprab 7425  df-mpo 7426

This theorem is used by:  ovmpos  7569  ov2gf  7570  ovmpodxf  7571  ovmpodf  7577  ovmpodv2  7579  xpcomco  9090  mapxpen  9166  pwfseqlem2  10748  pwfseqlem4a  10750  pwfseqlem4  10751  gsum2d2lem  20193  gsum2d2  20194  gsumcom2  20195  dprd2d2  20266  cnmpt21  23996  cnmpt2t  23998  cnmptcom  24003  cnmpt2k  24013  xkocnv  24139  finxpreclem2  38407  finxpreclem6  38413  mnringmulrcld  45320  fmuldfeq  46689  smflimlem6  47880  ovmpordxf  49545