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	$$⊢\forall x\left(x=t\to \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-ax12v	$$⊢\forall x\left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
2		equequ2	$$⊢y=t\to \left(x=y\leftrightarrow x=t\right)$$
3	2	imbi1d	$$⊢y=t\to \left(\left(x=y\to \phi \right)\leftrightarrow \left(x=t\to \phi \right)\right)$$
4	3	albidv	$$⊢y=t\to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x=t\to \phi \right)\right)$$
5	4	imbi2d	$$⊢y=t\to \left(\left(\phi \to \forall x\left(x=y\to \phi \right)\right)\leftrightarrow \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)$$
6	2 5	imbi12d	$$⊢y=t\to \left(\left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)\leftrightarrow \left(x=t\to \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)\right)$$
7	6	albidv	$$⊢y=t\to \left(\forall x\left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)\leftrightarrow \forall x\left(x=t\to \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)\right)$$
8	1 7	mpbii	$$⊢y=t\to \forall x\left(x=t\to \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)$$
9		ax6ev	$$⊢\exists yy=t$$
10	8 9	exlimiiv	$$⊢\forall x\left(x=t\to \left(\phi \to \forall x\left(x=t\to \phi \right)\right)\right)$$