This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 )
		ralxfr.2	⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
		ralxfr.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	ralxfrALT	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐶 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ralxfr.1	⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 )
2		ralxfr.2	⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3		ralxfr.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4	3	rspcv	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) )
5	1 4	syl	⊢ ( 𝑦 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → 𝜓 ) )
6	5	com12	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐶 → 𝜓 ) )
7	6	ralrimiv	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ 𝐶 𝜓 )
8		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐶 𝜓
9		nfv	⊢ Ⅎ 𝑦 𝜑
10		rsp	⊢ ( ∀ 𝑦 ∈ 𝐶 𝜓 → ( 𝑦 ∈ 𝐶 → 𝜓 ) )
11	3	biimprcd	⊢ ( 𝜓 → ( 𝑥 = 𝐴 → 𝜑 ) )
12	10 11	syl6	⊢ ( ∀ 𝑦 ∈ 𝐶 𝜓 → ( 𝑦 ∈ 𝐶 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
13	8 9 12	rexlimd	⊢ ( ∀ 𝑦 ∈ 𝐶 𝜓 → ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝜑 ) )
14	2 13	syl5	⊢ ( ∀ 𝑦 ∈ 𝐶 𝜓 → ( 𝑥 ∈ 𝐵 → 𝜑 ) )
15	14	ralrimiv	⊢ ( ∀ 𝑦 ∈ 𝐶 𝜓 → ∀ 𝑥 ∈ 𝐵 𝜑 )
16	7 15	impbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐶 𝜓 )