Metamath Proof Explorer

Theorem axuntco

Description: Derivation of ax-un from ax-tco . Use ax-un instead. (Contributed by Matthew House, 6-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-tco 
 |-  E. y ( x e. y /\ A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) )
2 elequ1 
 |-  ( v = x -> ( v e. y <-> x e. y ) )
3 elequ2 
 |-  ( v = x -> ( u e. v <-> u e. x ) )
4 3 imbi1d 
 |-  ( v = x -> ( ( u e. v -> u e. y ) <-> ( u e. x -> u e. y ) ) )
5 4 albidv 
 |-  ( v = x -> ( A. u ( u e. v -> u e. y ) <-> A. u ( u e. x -> u e. y ) ) )
6 2 5 imbi12d 
 |-  ( v = x -> ( ( v e. y -> A. u ( u e. v -> u e. y ) ) <-> ( x e. y -> A. u ( u e. x -> u e. y ) ) ) )
7 6 spvv 
 |-  ( A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) -> ( x e. y -> A. u ( u e. x -> u e. y ) ) )
8 elequ1 
 |-  ( u = w -> ( u e. x <-> w e. x ) )
9 elequ1 
 |-  ( u = w -> ( u e. y <-> w e. y ) )
10 8 9 imbi12d 
 |-  ( u = w -> ( ( u e. x -> u e. y ) <-> ( w e. x -> w e. y ) ) )
11 10 spvv 
 |-  ( A. u ( u e. x -> u e. y ) -> ( w e. x -> w e. y ) )
12 7 11 syl6 
 |-  ( A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) -> ( x e. y -> ( w e. x -> w e. y ) ) )
13 elequ1 
 |-  ( v = w -> ( v e. y <-> w e. y ) )
14 elequ2 
 |-  ( v = w -> ( u e. v <-> u e. w ) )
15 14 imbi1d 
 |-  ( v = w -> ( ( u e. v -> u e. y ) <-> ( u e. w -> u e. y ) ) )
16 15 albidv 
 |-  ( v = w -> ( A. u ( u e. v -> u e. y ) <-> A. u ( u e. w -> u e. y ) ) )
17 13 16 imbi12d 
 |-  ( v = w -> ( ( v e. y -> A. u ( u e. v -> u e. y ) ) <-> ( w e. y -> A. u ( u e. w -> u e. y ) ) ) )
18 17 spvv 
 |-  ( A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) -> ( w e. y -> A. u ( u e. w -> u e. y ) ) )
19 elequ1 
 |-  ( u = z -> ( u e. w <-> z e. w ) )
20 elequ1 
 |-  ( u = z -> ( u e. y <-> z e. y ) )
21 19 20 imbi12d 
 |-  ( u = z -> ( ( u e. w -> u e. y ) <-> ( z e. w -> z e. y ) ) )
22 21 spvv 
 |-  ( A. u ( u e. w -> u e. y ) -> ( z e. w -> z e. y ) )
23 18 22 syl6 
 |-  ( A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) -> ( w e. y -> ( z e. w -> z e. y ) ) )
24 12 23 syl6d 
 |-  ( A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) -> ( x e. y -> ( w e. x -> ( z e. w -> z e. y ) ) ) )
25 24 impcom 
 |-  ( ( x e. y /\ A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) ) -> ( w e. x -> ( z e. w -> z e. y ) ) )
26 25 impcomd 
 |-  ( ( x e. y /\ A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) ) -> ( ( z e. w /\ w e. x ) -> z e. y ) )
27 26 exlimdv 
 |-  ( ( x e. y /\ A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) ) -> ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
28 27 alrimiv 
 |-  ( ( x e. y /\ A. v ( v e. y -> A. u ( u e. v -> u e. y ) ) ) -> A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) )
29 1 28 eximii 
 |-  E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )