Theorem nfmpo1 7261

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

Syntax hints:   ∧ wa 399   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2880  {coprab 7184   ∈ cmpo 7185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-oprab 7187  df-mpo 7188

This theorem is referenced by:  ovmpos  7326  ov2gf  7327  ovmpodxf  7328  ovmpodf  7334  ovmpodv2  7336  xpcomco  8669  mapxpen  8746  pwfseqlem2  10172  pwfseqlem4a  10174  pwfseqlem4  10175  gsum2d2lem  19225  gsum2d2  19226  gsumcom2  19227  dprd2d2  19298  cnmpt21  22435  cnmpt2t  22437  cnmptcom  22442  cnmpt2k  22452  xkocnv  22578  numclwlk2lem2f1o  28329  finxpreclem2  35217  mnringmulrcld  41429  fmuldfeqlem1  42706  fmuldfeq  42707  ovmpordxf  45256