Metamath Proof Explorer

Theorem mh-prprimbi

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

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

Proof

Step Hyp Ref Expression
1 jaob 
 |-  ( ( ( w = x \/ w = y ) -> w e. z ) <-> ( ( w = x -> w e. z ) /\ ( w = y -> w e. z ) ) )
2 1 albii 
 |-  ( A. w ( ( w = x \/ w = y ) -> w e. z ) <-> A. w ( ( w = x -> w e. z ) /\ ( w = y -> w e. z ) ) )
3 19.26 
 |-  ( A. w ( ( w = x -> w e. z ) /\ ( w = y -> w e. z ) ) <-> ( A. w ( w = x -> w e. z ) /\ A. w ( w = y -> w e. z ) ) )
4 elequ1 
 |-  ( w = x -> ( w e. z <-> x e. z ) )
5 4 equsalvw 
 |-  ( A. w ( w = x -> w e. z ) <-> x e. z )
6 elequ1 
 |-  ( w = y -> ( w e. z <-> y e. z ) )
7 6 equsalvw 
 |-  ( A. w ( w = y -> w e. z ) <-> y e. z )
8 5 7 anbi12i 
 |-  ( ( A. w ( w = x -> w e. z ) /\ A. w ( w = y -> w e. z ) ) <-> ( x e. z /\ y e. z ) )
9 2 3 8 3bitri 
 |-  ( A. w ( ( w = x \/ w = y ) -> w e. z ) <-> ( x e. z /\ y e. z ) )
10 9 exbii 
 |-  ( E. z A. w ( ( w = x \/ w = y ) -> w e. z ) <-> E. z ( x e. z /\ y e. z ) )
11 exnalimn 
 |-  ( E. z ( x e. z /\ y e. z ) <-> -. A. z ( x e. z -> -. y e. z ) )
12 10 11 bitri 
 |-  ( E. z A. w ( ( w = x \/ w = y ) -> w e. z ) <-> -. A. z ( x e. z -> -. y e. z ) )