Theorem wl-equsal1i

Description: The antecedent x = y is irrelevant, if one or both setvar variables are not free in ph . (Contributed by Wolf Lammen, 1-Sep-2018)

	Ref	Expression
Hypotheses	wl-equsal1i.1	$$⊢\left(Ⅎx\phi \vee Ⅎy\phi \right)$$
	wl-equsal1i.2	$$⊢x=y\to \phi$$
Assertion	wl-equsal1i	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		wl-equsal1i.1	$$⊢\left(Ⅎx\phi \vee Ⅎy\phi \right)$$
2		wl-equsal1i.2	$$⊢x=y\to \phi$$
3	2	gen2	$$⊢\forall x\forall y\left(x=y\to \phi \right)$$
4		sp	$$⊢\forall y\forall x\left(x=y\to \phi \right)\to \forall x\left(x=y\to \phi \right)$$
5	4	alcoms	$$⊢\forall x\forall y\left(x=y\to \phi \right)\to \forall x\left(x=y\to \phi \right)$$
6		wl-equsal1t	$$⊢Ⅎx\phi \to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \phi \right)$$
7	5 6	syl5ib	$$⊢Ⅎx\phi \to \left(\forall x\forall y\left(x=y\to \phi \right)\to \phi \right)$$
8		wl-equsalcom	$$⊢\forall y\left(y=x\to \phi \right)\leftrightarrow \forall y\left(x=y\to \phi \right)$$
9		wl-equsal1t	$$⊢Ⅎy\phi \to \left(\forall y\left(y=x\to \phi \right)\leftrightarrow \phi \right)$$
10	9	biimpd	$$⊢Ⅎy\phi \to \left(\forall y\left(y=x\to \phi \right)\to \phi \right)$$
11	8 10	syl5bir	$$⊢Ⅎy\phi \to \left(\forall y\left(x=y\to \phi \right)\to \phi \right)$$
12	11	spsd	$$⊢Ⅎy\phi \to \left(\forall x\forall y\left(x=y\to \phi \right)\to \phi \right)$$
13	7 12	jaoi	$$⊢\left(Ⅎx\phi \vee Ⅎy\phi \right)\to \left(\forall x\forall y\left(x=y\to \phi \right)\to \phi \right)$$
14	1 3 13	mp2	$$⊢\phi$$