Metamath Proof Explorer

Theorem mh-unprimbi

Description: Shortest possible version of ax-un in primitive symbols. (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Assertion mh-unprimbi 
|- ( E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> -. A. y -. A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )

Proof

Step Hyp Ref Expression
1 elequ1 
 |-  ( v = z -> ( v e. u <-> z e. u ) )
2 elequ1 
 |-  ( v = z -> ( v e. y <-> z e. y ) )
3 2 imbi2d 
 |-  ( v = z -> ( ( u e. x -> v e. y ) <-> ( u e. x -> z e. y ) ) )
4 1 3 imbi12d 
 |-  ( v = z -> ( ( v e. u -> ( u e. x -> v e. y ) ) <-> ( z e. u -> ( u e. x -> z e. y ) ) ) )
5 elequ2 
 |-  ( u = w -> ( v e. u <-> v e. w ) )
6 elequ1 
 |-  ( u = w -> ( u e. x <-> w e. x ) )
7 6 imbi1d 
 |-  ( u = w -> ( ( u e. x -> v e. y ) <-> ( w e. x -> v e. y ) ) )
8 5 7 imbi12d 
 |-  ( u = w -> ( ( v e. u -> ( u e. x -> v e. y ) ) <-> ( v e. w -> ( w e. x -> v e. y ) ) ) )
9 4 8 alcomw 
 |-  ( A. v A. u ( v e. u -> ( u e. x -> v e. y ) ) <-> A. u A. v ( v e. u -> ( u e. x -> v e. y ) ) )
10 impexp 
 |-  ( ( ( z e. w /\ w e. x ) -> z e. y ) <-> ( z e. w -> ( w e. x -> z e. y ) ) )
11 elequ12 
 |-  ( ( z = v /\ w = u ) -> ( z e. w <-> v e. u ) )
12 elequ1 
 |-  ( w = u -> ( w e. x <-> u e. x ) )
13 12 adantl 
 |-  ( ( z = v /\ w = u ) -> ( w e. x <-> u e. x ) )
14 elequ1 
 |-  ( z = v -> ( z e. y <-> v e. y ) )
15 14 adantr 
 |-  ( ( z = v /\ w = u ) -> ( z e. y <-> v e. y ) )
16 13 15 imbi12d 
 |-  ( ( z = v /\ w = u ) -> ( ( w e. x -> z e. y ) <-> ( u e. x -> v e. y ) ) )
17 11 16 imbi12d 
 |-  ( ( z = v /\ w = u ) -> ( ( z e. w -> ( w e. x -> z e. y ) ) <-> ( v e. u -> ( u e. x -> v e. y ) ) ) )
18 10 17 bitrid 
 |-  ( ( z = v /\ w = u ) -> ( ( ( z e. w /\ w e. x ) -> z e. y ) <-> ( v e. u -> ( u e. x -> v e. y ) ) ) )
19 18 cbval2vw 
 |-  ( A. z A. w ( ( z e. w /\ w e. x ) -> z e. y ) <-> A. v A. u ( v e. u -> ( u e. x -> v e. y ) ) )
20 bi2.04 
 |-  ( ( z e. x -> ( w e. z -> w e. y ) ) <-> ( w e. z -> ( z e. x -> w e. y ) ) )
21 elequ12 
 |-  ( ( w = v /\ z = u ) -> ( w e. z <-> v e. u ) )
22 21 ancoms 
 |-  ( ( z = u /\ w = v ) -> ( w e. z <-> v e. u ) )
23 elequ1 
 |-  ( z = u -> ( z e. x <-> u e. x ) )
24 23 adantr 
 |-  ( ( z = u /\ w = v ) -> ( z e. x <-> u e. x ) )
25 elequ1 
 |-  ( w = v -> ( w e. y <-> v e. y ) )
26 25 adantl 
 |-  ( ( z = u /\ w = v ) -> ( w e. y <-> v e. y ) )
27 24 26 imbi12d 
 |-  ( ( z = u /\ w = v ) -> ( ( z e. x -> w e. y ) <-> ( u e. x -> v e. y ) ) )
28 22 27 imbi12d 
 |-  ( ( z = u /\ w = v ) -> ( ( w e. z -> ( z e. x -> w e. y ) ) <-> ( v e. u -> ( u e. x -> v e. y ) ) ) )
29 20 28 bitrid 
 |-  ( ( z = u /\ w = v ) -> ( ( z e. x -> ( w e. z -> w e. y ) ) <-> ( v e. u -> ( u e. x -> v e. y ) ) ) )
30 29 cbval2vw 
 |-  ( A. z A. w ( z e. x -> ( w e. z -> w e. y ) ) <-> A. u A. v ( v e. u -> ( u e. x -> v e. y ) ) )
31 9 19 30 3bitr4i 
 |-  ( A. z A. w ( ( z e. w /\ w e. x ) -> z e. y ) <-> A. z A. w ( z e. x -> ( w e. z -> w e. y ) ) )
32 19.23v 
 |-  ( A. w ( ( z e. w /\ w e. x ) -> z e. y ) <-> ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
33 32 albii 
 |-  ( A. z A. w ( ( z e. w /\ w e. x ) -> z e. y ) <-> A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
34 19.21v 
 |-  ( A. w ( z e. x -> ( w e. z -> w e. y ) ) <-> ( z e. x -> A. w ( w e. z -> w e. y ) ) )
35 34 albii 
 |-  ( A. z A. w ( z e. x -> ( w e. z -> w e. y ) ) <-> A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )
36 31 33 35 3bitr3i 
 |-  ( A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )
37 36 exbii 
 |-  ( E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> E. y A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )
38 df-ex 
 |-  ( E. y A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) <-> -. A. y -. A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )
39 37 38 bitri 
 |-  ( E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) <-> -. A. y -. A. z ( z e. x -> A. w ( w e. z -> w e. y ) ) )