Metamath Proof Explorer


Theorem elintima

Description: Element of intersection of images. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion elintima y x | a A x = a B a A b B b y a

Proof

Step Hyp Ref Expression
1 vex y V
2 1 elint2 y x | a A x = a B z x | a A x = a B y z
3 elequ2 z = x y z y x
4 3 ralab2 z x | a A x = a B y z x a A x = a B y x
5 df-rex a A x = a B a a A x = a B
6 5 imbi1i a A x = a B y x a a A x = a B y x
7 19.23v a a A x = a B y x a a A x = a B y x
8 simpr a A x = a B x = a B
9 8 eleq2d a A x = a B y x y a B
10 9 pm5.74i a A x = a B y x a A x = a B y a B
11 1 elima y a B b B b a y
12 df-br b a y b y a
13 12 rexbii b B b a y b B b y a
14 11 13 bitri y a B b B b y a
15 14 imbi2i a A x = a B y a B a A x = a B b B b y a
16 10 15 bitri a A x = a B y x a A x = a B b B b y a
17 16 albii a a A x = a B y x a a A x = a B b B b y a
18 6 7 17 3bitr2i a A x = a B y x a a A x = a B b B b y a
19 18 albii x a A x = a B y x x a a A x = a B b B b y a
20 19.23v x a A x = a B b B b y a x a A x = a B b B b y a
21 vex a V
22 21 imaex a B V
23 22 isseti x x = a B
24 19.42v x a A x = a B a A x x = a B
25 23 24 mpbiran2 x a A x = a B a A
26 25 imbi1i x a A x = a B b B b y a a A b B b y a
27 20 26 bitri x a A x = a B b B b y a a A b B b y a
28 27 albii a x a A x = a B b B b y a a a A b B b y a
29 alcom x a a A x = a B b B b y a a x a A x = a B b B b y a
30 df-ral a A b B b y a a a A b B b y a
31 28 29 30 3bitr4i x a a A x = a B b B b y a a A b B b y a
32 19 31 bitri x a A x = a B y x a A b B b y a
33 4 32 bitri z x | a A x = a B y z a A b B b y a
34 2 33 bitri y x | a A x = a B a A b B b y a