This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmrab

Description: Domain of a restricted class abstraction over a cartesian product. (Contributed by Thierry Arnoux, 3-Jul-2023)

Ref Expression
Hypothesis dmrab.1 
|- ( z = <. x , y >. -> ( ph <-> ps ) )
Assertion dmrab 
|- dom { z e. ( A X. B ) | ph } = { x e. A | E. y e. B ps }

Proof

Step Hyp Ref Expression
1 dmrab.1 
 |-  ( z = <. x , y >. -> ( ph <-> ps ) )
2 1 elrab 
 |-  ( <. x , y >. e. { z e. ( A X. B ) | ph } <-> ( <. x , y >. e. ( A X. B ) /\ ps ) )
3 opelxp 
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
4 3 anbi1i 
 |-  ( ( <. x , y >. e. ( A X. B ) /\ ps ) <-> ( ( x e. A /\ y e. B ) /\ ps ) )
5 ancom 
 |-  ( ( x e. A /\ y e. B ) <-> ( y e. B /\ x e. A ) )
6 5 anbi1i 
 |-  ( ( ( x e. A /\ y e. B ) /\ ps ) <-> ( ( y e. B /\ x e. A ) /\ ps ) )
7 2 4 6 3bitri 
 |-  ( <. x , y >. e. { z e. ( A X. B ) | ph } <-> ( ( y e. B /\ x e. A ) /\ ps ) )
8 anass 
 |-  ( ( ( y e. B /\ x e. A ) /\ ps ) <-> ( y e. B /\ ( x e. A /\ ps ) ) )
9 ancom 
 |-  ( ( x e. A /\ ps ) <-> ( ps /\ x e. A ) )
10 9 anbi2i 
 |-  ( ( y e. B /\ ( x e. A /\ ps ) ) <-> ( y e. B /\ ( ps /\ x e. A ) ) )
11 7 8 10 3bitri 
 |-  ( <. x , y >. e. { z e. ( A X. B ) | ph } <-> ( y e. B /\ ( ps /\ x e. A ) ) )
12 11 exbii 
 |-  ( E. y <. x , y >. e. { z e. ( A X. B ) | ph } <-> E. y ( y e. B /\ ( ps /\ x e. A ) ) )
13 df-rex 
 |-  ( E. y e. B ( ps /\ x e. A ) <-> E. y ( y e. B /\ ( ps /\ x e. A ) ) )
14 r19.41v 
 |-  ( E. y e. B ( ps /\ x e. A ) <-> ( E. y e. B ps /\ x e. A ) )
15 12 13 14 3bitr2i 
 |-  ( E. y <. x , y >. e. { z e. ( A X. B ) | ph } <-> ( E. y e. B ps /\ x e. A ) )
16 15 biancomi 
 |-  ( E. y <. x , y >. e. { z e. ( A X. B ) | ph } <-> ( x e. A /\ E. y e. B ps ) )
17 16 abbii 
 |-  { x | E. y <. x , y >. e. { z e. ( A X. B ) | ph } } = { x | ( x e. A /\ E. y e. B ps ) }
18 dfdm3 
 |-  dom { z e. ( A X. B ) | ph } = { x | E. y <. x , y >. e. { z e. ( A X. B ) | ph } }
19 df-rab 
 |-  { x e. A | E. y e. B ps } = { x | ( x e. A /\ E. y e. B ps ) }
20 17 18 19 3eqtr4i 
 |-  dom { z e. ( A X. B ) | ph } = { x e. A | E. y e. B ps }