Theorem axc11r

Description: Same as axc11 but with reversed antecedent. Note the use of ax-12 (and not merely ax12v as in axc11rv ).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev and aecom , for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015)

	Ref	Expression
Assertion	axc11r	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-12	$$⊢y=x\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
2	1	sps	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
3		pm2.27	$$⊢y=x\to \left(\left(y=x\to \phi \right)\to \phi \right)$$
4	3	al2imi	$$⊢\forall yy=x\to \left(\forall y\left(y=x\to \phi \right)\to \forall y\phi \right)$$
5	2 4	syld	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$