Theorem dral1

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker dral1v if possible. (Contributed by NM, 24-Nov-1994) Remove dependency on ax-11 . (Revised by Wolf Lammen, 6-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	dral1.1	$$⊢\forall xx=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	dral1	$$⊢\forall xx=y\to \left(\forall x\phi \leftrightarrow \forall y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dral1.1	$$⊢\forall xx=y\to \left(\phi \leftrightarrow \psi \right)$$
2		nfa1	$$⊢Ⅎx\forall xx=y$$
3	2 1	albid	$$⊢\forall xx=y\to \left(\forall x\phi \leftrightarrow \forall x\psi \right)$$
4		axc11	$$⊢\forall xx=y\to \left(\forall x\psi \to \forall y\psi \right)$$
5		axc11r	$$⊢\forall xx=y\to \left(\forall y\psi \to \forall x\psi \right)$$
6	4 5	impbid	$$⊢\forall xx=y\to \left(\forall x\psi \leftrightarrow \forall y\psi \right)$$
7	3 6	bitrd	$$⊢\forall xx=y\to \left(\forall x\phi \leftrightarrow \forall y\psi \right)$$