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

Metamath Proof Explorer

Theorem raliunxp

Description: Write a double restricted quantification as one universal quantifier. In this version of ralxp , B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis ralxp.1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion raliunxp ( ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜓 )

Proof

Step Hyp Ref Expression
1 ralxp.1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2 eliunxp ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
3 2 imbi1i ⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) → 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) )
4 19.23vv ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) )
5 3 4 bitr4i ⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) )
6 5 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) )
7 alrot3 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) )
8 impexp ⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜑 ) ) )
9 8 albii ⊢ ( ∀ 𝑥 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜑 ) ) )
10 opex ⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
11 1 imbi2d ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) ) )
12 10 11 ceqsalv ⊢ ( ∀ 𝑥 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜑 ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
13 9 12 bitri ⊢ ( ∀ 𝑥 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
14 13 2albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
15 7 14 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
16 6 15 bitri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
17 df-ral ⊢ ( ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) → 𝜑 ) )
18 r2al ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝜓 ) )
19 16 17 18 3bitr4i ⊢ ( ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 𝜓 )