Theorem nfmpo2 7492

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Ⅎwnfc 2883  {coprab 7412   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  ovmpos  7558  ov2gf  7559  ovmpodxf  7560  ovmpodf  7566  ovmpodv2  7568  xpcomco  9064  mapxpen  9145  pwfseqlem2  10656  pwfseqlem4a  10658  pwfseqlem4  10659  gsum2d2lem  19882  gsum2d2  19883  gsumcom2  19884  dprd2d2  19955  cnmpt21  23395  cnmpt2t  23397  cnmptcom  23402  cnmpt2k  23412  xkocnv  23538  finxpreclem2  36574  finxpreclem6  36580  mnringmulrcld  43289  fmuldfeq  44598  smflimlem6  45791  ovmpordxf  47103