Theorem fnopab2 3618

Description: Functionality and domain of an ordered-pair class abstraction.

Hypotheses

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

Assertion

Ref	Expression
fnopab2	|- F Fn A

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

Proof of Theorem fnopab2

Step	Hyp	Ref	Expression
1		fnopab2.1	. . . 4 |- B e. V
2	1	eueq1 1917	. . 3 |- E!y y = B
3	2	a1i 8	. 2 |- (x e. A -> E!y y = B)
4		fnopab2.2	. 2 |- F = {<.x, y>. | (x e. A /\ y = B)}
5	3, 4	fnopab 3617	1 |- F Fn A

Syntax hints:   /\ wa 223   = wceq 956   e. wcel 958  E!weu 1380  Vcvv 1811  {copab 2666   Fn wfn 3177

This theorem is referenced by:  dmopab2 3619  fnopabfv 3758  rnssopab 3825  fopabco 3832  fopabcos 3833  fopabsn 3840  funiunfv 3866  fo1st 4091  fo2nd 4092  curry1 4098  pw2en 4446  mapxpen 4495  unfilem2 4549  pwfilemOLD 4570  aceq3lem 4732  aceq4 4734  ac6lem 4754  iundom 4812  cffnon 4907  seq1fnlem 6313  shftfn 6343  ref 6759  imf 6760  caucvg3 7167  cvgcmp2 7181  cvgcmp2c 7183  cvgcmp3ce 7187  geolimi 7236  eff 7313  reeff1o 7426  sinf 7440  cosf 7441  0vfval 8225  vsfval 8254  ipasslem8 8497  ubthlem6 8534  htthlem11 8630  sincolem 8665  efghgrpilem 8719  efif 8721  shftefif1olem 8741  pjfn 9646  pjmfn 9660  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-sep 2703  ax-pow 2742  ax-pr 2779

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-ral 1649  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-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-fun 3192  df-fn 3193

Copyright terms: Public domain