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

Metamath Proof Explorer

Theorem ralxfrd2

Description: Transfer universal quantification from a variable x to another variable y contained in expression A . Variant of ralxfrd . (Contributed by Alexander van der Vekens, 25-Apr-2018)

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

Proof

Step Hyp Ref Expression
1 ralxfrd2.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
2 ralxfrd2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3 ralxfrd2.3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4 3 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
5 1 4 rspcdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐵 𝜓 → 𝜒 ) )
6 5 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 → ∀ 𝑦 ∈ 𝐶 𝜒 ) )
7 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐶 𝜒 ∧ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) → ∃ 𝑦 ∈ 𝐶 ( 𝜒 ∧ 𝑥 = 𝐴 ) )
8 3 ad4ant134 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
9 8 exbiri ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 = 𝐴 → ( 𝜒 → 𝜓 ) ) )
10 9 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝜒 ∧ 𝑥 = 𝐴 ) → 𝜓 ) )
11 10 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐶 ( 𝜒 ∧ 𝑥 = 𝐴 ) → 𝜓 ) )
12 7 11 syl5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝐶 𝜒 ∧ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) → 𝜓 ) )
13 2 12 mpan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐶 𝜒 → 𝜓 ) )
14 13 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐶 𝜒 → ∀ 𝑥 ∈ 𝐵 𝜓 ) )
15 6 14 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 𝜒 ) )