Metamath Proof Explorer


Theorem dmopab2rex

Description: The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023)

Ref Expression
Assertion dmopab2rex u U v V B X i I D W dom x y | u U v V x = A y = B i I x = C y = D = x | u U v V x = A i I x = C

Proof

Step Hyp Ref Expression
1 rexcom4 v V y z = A y = B y v V z = A y = B
2 rexcom4 i I y z = C y = D y i I z = C y = D
3 1 2 orbi12i v V y z = A y = B i I y z = C y = D y v V z = A y = B y i I z = C y = D
4 19.43 y v V z = A y = B i I z = C y = D y v V z = A y = B y i I z = C y = D
5 3 4 bitr4i v V y z = A y = B i I y z = C y = D y v V z = A y = B i I z = C y = D
6 5 rexbii u U v V y z = A y = B i I y z = C y = D u U y v V z = A y = B i I z = C y = D
7 rexcom4 u U y v V z = A y = B i I z = C y = D y u U v V z = A y = B i I z = C y = D
8 6 7 bitri u U v V y z = A y = B i I y z = C y = D y u U v V z = A y = B i I z = C y = D
9 simpl z = A y = B z = A
10 9 exlimiv y z = A y = B z = A
11 elisset B X y y = B
12 ibar z = A y = B z = A y = B
13 12 bicomd z = A z = A y = B y = B
14 13 exbidv z = A y z = A y = B y y = B
15 11 14 syl5ibrcom B X z = A y z = A y = B
16 10 15 impbid2 B X y z = A y = B z = A
17 16 ralrexbid v V B X v V y z = A y = B v V z = A
18 17 adantr v V B X i I D W v V y z = A y = B v V z = A
19 simpl z = C y = D z = C
20 19 exlimiv y z = C y = D z = C
21 elisset D W y y = D
22 ibar z = C y = D z = C y = D
23 22 bicomd z = C z = C y = D y = D
24 23 exbidv z = C y z = C y = D y y = D
25 21 24 syl5ibrcom D W z = C y z = C y = D
26 20 25 impbid2 D W y z = C y = D z = C
27 26 ralrexbid i I D W i I y z = C y = D i I z = C
28 27 adantl v V B X i I D W i I y z = C y = D i I z = C
29 18 28 orbi12d v V B X i I D W v V y z = A y = B i I y z = C y = D v V z = A i I z = C
30 29 ralrexbid u U v V B X i I D W u U v V y z = A y = B i I y z = C y = D u U v V z = A i I z = C
31 8 30 bitr3id u U v V B X i I D W y u U v V z = A y = B i I z = C y = D u U v V z = A i I z = C
32 eqeq1 x = z x = A z = A
33 32 anbi1d x = z x = A y = B z = A y = B
34 33 rexbidv x = z v V x = A y = B v V z = A y = B
35 eqeq1 x = z x = C z = C
36 35 anbi1d x = z x = C y = D z = C y = D
37 36 rexbidv x = z i I x = C y = D i I z = C y = D
38 34 37 orbi12d x = z v V x = A y = B i I x = C y = D v V z = A y = B i I z = C y = D
39 38 rexbidv x = z u U v V x = A y = B i I x = C y = D u U v V z = A y = B i I z = C y = D
40 39 dmopabelb z V z dom x y | u U v V x = A y = B i I x = C y = D y u U v V z = A y = B i I z = C y = D
41 40 elv z dom x y | u U v V x = A y = B i I x = C y = D y u U v V z = A y = B i I z = C y = D
42 vex z V
43 32 rexbidv x = z v V x = A v V z = A
44 35 rexbidv x = z i I x = C i I z = C
45 43 44 orbi12d x = z v V x = A i I x = C v V z = A i I z = C
46 45 rexbidv x = z u U v V x = A i I x = C u U v V z = A i I z = C
47 42 46 elab z x | u U v V x = A i I x = C u U v V z = A i I z = C
48 31 41 47 3bitr4g u U v V B X i I D W z dom x y | u U v V x = A y = B i I x = C y = D z x | u U v V x = A i I x = C
49 48 eqrdv u U v V B X i I D W dom x y | u U v V x = A y = B i I x = C y = D = x | u U v V x = A i I x = C