Theorem nfmpo2 7481

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

Syntax hints:   ∧ wa 400   = wceq 1563   ∈ wcel 2145  Ⅎwnfc 2912  {coprab 7401   ∈ cmpo 7402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-oprab 7404  df-mpo 7405

This theorem is referenced by:  ovmpos  7548  ov2gf  7549  ovmpodxf  7550  ovmpodf  7556  ovmpodv2  7558  xpcomco  9043  mapxpen  9119  pwfseqlem2  10632  pwfseqlem4a  10634  pwfseqlem4  10635  gsum2d2lem  20034  gsum2d2  20035  gsumcom2  20036  dprd2d2  20107  cnmpt21  23789  cnmpt2t  23791  cnmptcom  23796  cnmpt2k  23806  xkocnv  23932  finxpreclem2  37896  finxpreclem6  37902  mnringmulrcld  44816  fmuldfeq  46157  smflimlem6  47348  ovmpordxf  48970