Metamath Proof Explorer

Theorem bj-ax12

Description: Remove a DV condition from bj-ax12v (using core axioms only). (Contributed by BJ, 26-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ax12 
|- A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) )

Proof

Step Hyp Ref Expression
1 bj-ax12v 
 |-  A. x ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
2 equequ2 
 |-  ( y = t -> ( x = y <-> x = t ) )
3 2 imbi1d 
 |-  ( y = t -> ( ( x = y -> ph ) <-> ( x = t -> ph ) ) )
4 3 albidv 
 |-  ( y = t -> ( A. x ( x = y -> ph ) <-> A. x ( x = t -> ph ) ) )
5 4 imbi2d 
 |-  ( y = t -> ( ( ph -> A. x ( x = y -> ph ) ) <-> ( ph -> A. x ( x = t -> ph ) ) ) )
6 2 5 imbi12d 
 |-  ( y = t -> ( ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) <-> ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) ) )
7 6 albidv 
 |-  ( y = t -> ( A. x ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) <-> A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) ) )
8 1 7 mpbii 
 |-  ( y = t -> A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) )
9 ax6ev 
 |-  E. y y = t
10 8 9 exlimiiv 
 |-  A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) )