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 vex y V
3 2 elima y F A x A x F y
4 eqcom y = F x F x = y
5 ssel A dom F x A x dom F
6 funbrfvb Fun F x dom F F x = y x F y
7 6 ex Fun F x dom F F x = y x F y
8 5 7 syl9 A dom F Fun F x A F x = y x F y
9 8 imp31 A dom F Fun F x A F x = y x F y
10 4 9 syl5bb A dom F Fun F x A y = F x x F y
11 10 rexbidva A dom F Fun F x A y = F x x A x F y
12 3 11 bitr4id 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 bitr4di 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 bitrdi 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