Theorem nfmpt1 4122

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)

Assertion

Ref	Expression
nfmpt1	|- F/_ x ( x e. A |-> B )

Proof of Theorem nfmpt1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 4092	. 2 |- ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
2		nfopab1 4098	. 2 |- F/_ x { <. x , z >. | ( x e. A /\ z = B ) }
3	1, 2	nfcxfr 2333	1 |- F/_ x ( x e. A |-> B )

Syntax hints:   /\ wa 104   = wceq 1364   e. wcel 2164   F/_wnfc 2323   {copab 4089   |-> cmpt 4090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-opab 4091  df-mpt 4092

This theorem is referenced by:  nffvmpt1  5565  fvmptss2  5632  fvmptssdm  5642  fvmptdf  5645  mpteqb  5648  fvmptf  5650  ralrnmpt  5700  rexrnmpt  5701  f1ompt  5709  f1mpt  5814  fliftfun  5839  dom2lem  6826  mapxpen  6904  mkvprop  7217  cc3  7328  nfcprod1  11697  cnmpt11  14451  lgseisenlem2  15187