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

Metamath Proof Explorer

Theorem ralxfr2d

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by Mario Carneiro, 20-Aug-2014)

		Ref	Expression
	Hypotheses	ralxfr2d.1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 )
		ralxfr2d.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) )
		ralxfr2d.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
	Assertion	ralxfr2d	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralxfr2d.1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 )
2		ralxfr2d.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) )
3		ralxfr2d.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
5	1 4	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑥 𝑥 = 𝐴 )
6	2	biimprd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
7		r19.23v	⊢ ( ∀ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
8	6 7	sylibr	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
9	8	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
10		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
11	9 10	mpbidi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
12	11	exlimdv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
13	5 12	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
14	2	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
15	13 14 3	ralxfrd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 𝜒 ) )