Metamath Proof Explorer

Theorem regsfromsetind

Description: Derivation of ax-regs from mh-setind . (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Hypothesis regsfromsetind.1 
|- ( A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) -> -. ph )
Assertion regsfromsetind 
|- ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )

Proof

Step Hyp Ref Expression
1 regsfromsetind.1 
 |-  ( A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) -> -. ph )
2 nfia1 
 |-  F/ x ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) )
3 2 nfal 
 |-  F/ x A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) )
4 3 nfn 
 |-  F/ x -. A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) )
5 1 con2i 
 |-  ( ph -> -. A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) )
6 4 5 exlimi 
 |-  ( E. x ph -> -. A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) )
7 exnalimn 
 |-  ( E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) <-> -. A. y ( A. x ( x = y -> ph ) -> -. A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
8 nfv 
 |-  F/ z ( x e. y -> -. ph )
9 nfv 
 |-  F/ x z e. y
10 nfna1 
 |-  F/ x -. A. x ( x = z -> ph )
11 9 10 nfim 
 |-  F/ x ( z e. y -> -. A. x ( x = z -> ph ) )
12 elequ1 
 |-  ( x = z -> ( x e. y <-> z e. y ) )
13 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
14 sb6 
 |-  ( [ z / x ] ph <-> A. x ( x = z -> ph ) )
15 13 14 bitrdi 
 |-  ( x = z -> ( ph <-> A. x ( x = z -> ph ) ) )
16 15 notbid 
 |-  ( x = z -> ( -. ph <-> -. A. x ( x = z -> ph ) ) )
17 12 16 imbi12d 
 |-  ( x = z -> ( ( x e. y -> -. ph ) <-> ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
18 8 11 17 cbvalv1 
 |-  ( A. x ( x e. y -> -. ph ) <-> A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
19 alinexa 
 |-  ( A. x ( x = y -> -. ph ) <-> -. E. x ( x = y /\ ph ) )
20 sbalex 
 |-  ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
21 19 20 xchbinx 
 |-  ( A. x ( x = y -> -. ph ) <-> -. A. x ( x = y -> ph ) )
22 18 21 imbi12i 
 |-  ( ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) <-> ( A. z ( z e. y -> -. A. x ( x = z -> ph ) ) -> -. A. x ( x = y -> ph ) ) )
23 con2b 
 |-  ( ( A. z ( z e. y -> -. A. x ( x = z -> ph ) ) -> -. A. x ( x = y -> ph ) ) <-> ( A. x ( x = y -> ph ) -> -. A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
24 22 23 bitri 
 |-  ( ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) <-> ( A. x ( x = y -> ph ) -> -. A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
25 24 albii 
 |-  ( A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) <-> A. y ( A. x ( x = y -> ph ) -> -. A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
26 7 25 xchbinxr 
 |-  ( E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) <-> -. A. y ( A. x ( x e. y -> -. ph ) -> A. x ( x = y -> -. ph ) ) )
27 6 26 sylibr 
 |-  ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )