Metamath Proof Explorer

Theorem axregs

Description: Derivation of ax-regs from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025)

Ref Expression
Assertion axregs 
|- ( 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 zfregs2 
 |-  ( { x | ph } =/= (/) -> -. A. y e. { x | ph } E. z ( z e. { x | ph } /\ z e. y ) )
2 abn0 
 |-  ( { x | ph } =/= (/) <-> E. x ph )
3 df-ral 
 |-  ( A. y e. { x | ph } E. z ( z e. { x | ph } /\ z e. y ) <-> A. y ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) )
4 3 notbii 
 |-  ( -. A. y e. { x | ph } E. z ( z e. { x | ph } /\ z e. y ) <-> -. A. y ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) )
5 exnal 
 |-  ( E. y -. ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) <-> -. A. y ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) )
6 annim 
 |-  ( ( y e. { x | ph } /\ -. E. z ( z e. { x | ph } /\ z e. y ) ) <-> -. ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) )
7 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
8 sb6 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
9 7 8 bitri 
 |-  ( y e. { x | ph } <-> A. x ( x = y -> ph ) )
10 df-clab 
 |-  ( z e. { x | ph } <-> [ z / x ] ph )
11 sb6 
 |-  ( [ z / x ] ph <-> A. x ( x = z -> ph ) )
12 10 11 bitri 
 |-  ( z e. { x | ph } <-> A. x ( x = z -> ph ) )
13 12 anbi2ci 
 |-  ( ( z e. { x | ph } /\ z e. y ) <-> ( z e. y /\ A. x ( x = z -> ph ) ) )
14 df-an 
 |-  ( ( z e. y /\ A. x ( x = z -> ph ) ) <-> -. ( z e. y -> -. A. x ( x = z -> ph ) ) )
15 13 14 bitri 
 |-  ( ( z e. { x | ph } /\ z e. y ) <-> -. ( z e. y -> -. A. x ( x = z -> ph ) ) )
16 15 con2bii 
 |-  ( ( z e. y -> -. A. x ( x = z -> ph ) ) <-> -. ( z e. { x | ph } /\ z e. y ) )
17 16 albii 
 |-  ( A. z ( z e. y -> -. A. x ( x = z -> ph ) ) <-> A. z -. ( z e. { x | ph } /\ z e. y ) )
18 alnex 
 |-  ( A. z -. ( z e. { x | ph } /\ z e. y ) <-> -. E. z ( z e. { x | ph } /\ z e. y ) )
19 17 18 bitr2i 
 |-  ( -. E. z ( z e. { x | ph } /\ z e. y ) <-> A. z ( z e. y -> -. A. x ( x = z -> ph ) ) )
20 9 19 anbi12i 
 |-  ( ( y e. { x | ph } /\ -. E. z ( z e. { x | ph } /\ z e. y ) ) <-> ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
21 6 20 bitr3i 
 |-  ( -. ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) <-> ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
22 21 exbii 
 |-  ( E. y -. ( y e. { x | ph } -> E. z ( z e. { x | ph } /\ z e. y ) ) <-> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
23 4 5 22 3bitr2i 
 |-  ( -. A. y e. { x | ph } E. z ( z e. { x | ph } /\ z e. y ) <-> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )
24 1 2 23 3imtr3i 
 |-  ( E. x ph -> E. y ( A. x ( x = y -> ph ) /\ A. z ( z e. y -> -. A. x ( x = z -> ph ) ) ) )