Metamath Proof Explorer


Theorem elinintrab

Description: Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020)

Ref Expression
Assertion elinintrab A V A w 𝒫 B | x w = B x φ x φ A B x φ A x

Proof

Step Hyp Ref Expression
1 vex x V
2 1 inex2 B x V
3 inss1 B x B
4 2 3 elmapintrab A V A w 𝒫 B | x w = B x φ x φ A B x φ A B x
5 elin A B x A B A x
6 5 imbi2i φ A B x φ A B A x
7 jcab φ A B A x φ A B φ A x
8 6 7 bitri φ A B x φ A B φ A x
9 8 albii x φ A B x x φ A B φ A x
10 19.26 x φ A B φ A x x φ A B x φ A x
11 19.23v x φ A B x φ A B
12 11 anbi1i x φ A B x φ A x x φ A B x φ A x
13 10 12 bitri x φ A B φ A x x φ A B x φ A x
14 9 13 bitri x φ A B x x φ A B x φ A x
15 14 anbi2i x φ A B x φ A B x x φ A B x φ A B x φ A x
16 anabs5 x φ A B x φ A B x φ A x x φ A B x φ A x
17 15 16 bitri x φ A B x φ A B x x φ A B x φ A x
18 4 17 bitrdi A V A w 𝒫 B | x w = B x φ x φ A B x φ A x