Metamath Proof Explorer


Theorem funimass4

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion funimass4 Fun F A dom F F A B x A F x B

Proof

Step Hyp Ref Expression
1 dfss2 F A B y y F A y B
2 eqcom y = F x F x = y
3 ssel A dom F x A x dom F
4 funbrfvb Fun F x dom F F x = y x F y
5 4 ex Fun F x dom F F x = y x F y
6 3 5 syl9 A dom F Fun F x A F x = y x F y
7 6 imp31 A dom F Fun F x A F x = y x F y
8 2 7 syl5bb A dom F Fun F x A y = F x x F y
9 8 rexbidva A dom F Fun F x A y = F x x A x F y
10 vex y V
11 10 elima y F A x A x F y
12 9 11 syl6rbbr A dom F Fun F y F A x A y = F x
13 12 imbi1d A dom F Fun F y F A y B x A y = F x y B
14 r19.23v x A y = F x y B x A y = F x y B
15 13 14 syl6bbr A dom F Fun F y F A y B x A y = F x y B
16 15 albidv A dom F Fun F y y F A y B y x A y = F x y B
17 ralcom4 x A y y = F x y B y x A y = F x y B
18 fvex F x V
19 eleq1 y = F x y B F x B
20 18 19 ceqsalv y y = F x y B F x B
21 20 ralbii x A y y = F x y B x A F x B
22 17 21 bitr3i y x A y = F x y B x A F x B
23 16 22 syl6bb A dom F Fun F y y F A y B x A F x B
24 1 23 syl5bb A dom F Fun F F A B x A F x B
25 24 ancoms Fun F A dom F F A B x A F x B