This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ x x = t → φ → ∀ x x = t → φ

Proof

Step Hyp Ref Expression
1 bj-ax12v ⊢ ∀ x x = y → φ → ∀ x x = y → φ
2 equequ2 ⊢ y = t → x = y ↔ x = t
3 2 imbi1d ⊢ y = t → x = y → φ ↔ x = t → φ
4 3 albidv ⊢ y = t → ∀ x x = y → φ ↔ ∀ x x = t → φ
5 4 imbi2d ⊢ y = t → φ → ∀ x x = y → φ ↔ φ → ∀ x x = t → φ
6 2 5 imbi12d ⊢ y = t → x = y → φ → ∀ x x = y → φ ↔ x = t → φ → ∀ x x = t → φ
7 6 albidv ⊢ y = t → ∀ x x = y → φ → ∀ x x = y → φ ↔ ∀ x x = t → φ → ∀ x x = t → φ
8 1 7 mpbii ⊢ y = t → ∀ x x = t → φ → ∀ x x = t → φ
9 ax6ev ⊢ ∃ y y = t
10 8 9 exlimiiv ⊢ ∀ x x = t → φ → ∀ x x = t → φ