Theorem ralxfrALT

Description: Alternate proof of ralxfr which does not use ralxfrd . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ralxfr.1	$$⊢y\in C\to A\in B$$
	ralxfr.2	$$⊢x\in B\to \exists y\in Cx=A$$
	ralxfr.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralxfrALT	$$⊢\forall x\in B\phi \leftrightarrow \forall y\in C\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxfr.1	$$⊢y\in C\to A\in B$$
2		ralxfr.2	$$⊢x\in B\to \exists y\in Cx=A$$
3		ralxfr.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4	3	rspcv	$$⊢A\in B\to \left(\forall x\in B\phi \to \psi \right)$$
5	1 4	syl	$$⊢y\in C\to \left(\forall x\in B\phi \to \psi \right)$$
6	5	com12	$$⊢\forall x\in B\phi \to \left(y\in C\to \psi \right)$$
7	6	ralrimiv	$$⊢\forall x\in B\phi \to \forall y\in C\psi$$
8		nfra1	$$⊢Ⅎy\forall y\in C\psi$$
9		nfv	$$⊢Ⅎy\phi$$
10		rsp	$$⊢\forall y\in C\psi \to \left(y\in C\to \psi \right)$$
11	3	biimprcd	$$⊢\psi \to \left(x=A\to \phi \right)$$
12	10 11	syl6	$$⊢\forall y\in C\psi \to \left(y\in C\to \left(x=A\to \phi \right)\right)$$
13	8 9 12	rexlimd	$$⊢\forall y\in C\psi \to \left(\exists y\in Cx=A\to \phi \right)$$
14	2 13	syl5	$$⊢\forall y\in C\psi \to \left(x\in B\to \phi \right)$$
15	14	ralrimiv	$$⊢\forall y\in C\psi \to \forall x\in B\phi$$
16	7 15	impbii	$$⊢\forall x\in B\phi \leftrightarrow \forall y\in C\psi$$