Theorem mptexg 5149

Description: If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.)

Assertion

Ref	Expression
mptexg	|- (A e. V -> (x e. A |-> B) e. _V)

Distinct variable group:   x,A

Proof of Theorem mptexg

Step	Hyp	Ref	Expression
1		df-mpt 5138	. 2 |- (x e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}
2		opabex2g 4675	. 2 |- (A e. V -> {<.x, y>. | (x e. A /\ y = B)} e. _V)
3	1, 2	syl5eqel 2251	1 |- (A e. V -> (x e. A |-> B) e. _V)

Syntax hints:   -> wi 3   /\ wa 433   = wceq 1615   e. wcel 1617  _Vcvv 2569  {copab 3597   e. cmpt 5136

This theorem is referenced by:  unxpdomlem3 5863  noinfep 6027  coftr 6355  axcc3 6362  axcc3OLD 6364  axdc2lem 6374  axcclem 6383  konigthlem 6504  konigthlemOLD 6506  rpnnen1lem1 9289  rpnnen1lem3 9291  rpnnen1lem5 9293  rpnnen2lem1 9295  rpnnen2lem2 9296  rpnnen2lem3 9297  rpnnen2lem9 9303  grpinvfval 9640  lubfval 9722  glbfval 9727  circumlem2 14643  cbicplem 15508  grphmlem0 16029  grphmlem1 16030  grphlem3 16032  grphm 16035  ocvfval 18186  pmapfval 18460  polfval 18593  watfval 18677  ldilfset 18742  ltrnfset 18751  dilfset 18783  trnfset 18786  trlfset 18791  trlset 18792  tgrpfset 19416  tendofset 19428  tendopl 19441  tendoi 19456  edringfset 19458

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-rex 2390  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-mpt 5138

Copyright terms: Public domain