Theorem nfmpo1 7364

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Ⅎwnfc 2888  {coprab 7285   ∈ cmpo 7286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-oprab 7288  df-mpo 7289

This theorem is referenced by:  ovmpos  7430  ov2gf  7431  ovmpodxf  7432  ovmpodf  7438  ovmpodv2  7440  xpcomco  8858  mapxpen  8939  pwfseqlem2  10424  pwfseqlem4a  10426  pwfseqlem4  10427  gsum2d2lem  19583  gsum2d2  19584  gsumcom2  19585  dprd2d2  19656  cnmpt21  22831  cnmpt2t  22833  cnmptcom  22838  cnmpt2k  22848  xkocnv  22974  numclwlk2lem2f1o  28752  finxpreclem2  35570  mnringmulrcld  41853  fmuldfeqlem1  43130  fmuldfeq  43131  ovmpordxf  45685