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 }