Theorem nfmpt21 6722

Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013.)

Assertion

Ref	Expression
nfmpt21	⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Proof of Theorem nfmpt21

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt2 6655	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
2		nfoprab1 6704	. 2 ⊢ Ⅎ𝑥{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
3	1, 2	nfcxfr 2762	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Ⅎwnfc 2751  {coprab 6651   ↦ cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  ovmpt2s  6784  ov2gf  6785  ovmpt2dxf  6786  ovmpt2df  6792  ovmpt2dv2  6794  xpcomco  8050  mapxpen  8126  pwfseqlem2  9481  pwfseqlem4a  9483  pwfseqlem4  9484  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  dprd2d2  18443  cnmpt21  21474  cnmpt2t  21476  cnmptcom  21481  cnmpt2k  21491  xkocnv  21617  numclwlk2lem2f1o  27238  finxpreclem2  33227  fmuldfeqlem1  39814  fmuldfeq  39815  ovmpt2rdxf  42117