Theorem opabex2 3610

Description: Existence of a function expressed as class of ordered pairs.

Hypothesis

Ref	Expression
opabex2.1	|- A e. V

Assertion

Ref	Expression
opabex2	|- {<.x, y>. | (x e. A /\ y = B)} e. V

Distinct variable groups:   x,y,A   y,B

Proof of Theorem opabex2

Step	Hyp	Ref	Expression
1		opabex2.1	. 2 |- A e. V
2		moeq 1920	. . 3 |- E*y y = B
3	2	a1i 8	. 2 |- (x e. A -> E*y y = B)
4	1, 3	opabex 3609	1 |- {<.x, y>. | (x e. A /\ y = B)} e. V

Syntax hints:   /\ wa 223   = wceq 956   e. wcel 958  E*wmo 1381  Vcvv 1811  {copab 2666

This theorem is referenced by:  fopabex2 3612  pw2en 4446  mapxpen 4495  xpmapenlem2 4497  aceq4 4734  aceq6a 4741  seq1val 6312  shftfval 6342  seqzres2 6561  fsum1 7005  fsump1 7006  climsub 7130  iserzabs 7179  isumclim3t 7200  isummulc1 7212  isummulc1ALT 7213  infcvg 7224  geolim1i 7238  geosum 7241  geoisum 7242  geoisum1 7244  geoisum1c 7245  dfef2 7307  efclt 7312  efcvgfsum 7315  reefcl 7317  efcj 7336  efge1 7401  efge1p 7402  absefm1le 7412  lmfex 7959  addcn 7986  subcn 7987  mulcn 7988  sqcn 8335  nmofval 8425  minveceu 8583  htthlem3 8622  htthlem11 8630  pjmvalt 9238  hosmvalt 9511  hommvalt 9512  hodmvalt 9513  hfsmvalt 9514  hfmmvalt 9515  pjmfn 9660  eigvalvalt 9823  bravalt 9867  kbvalt 9876  rnbra 10040  bra11 10041

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193

Copyright terms: Public domain