# 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 ( ∀ 𝑥 𝑦𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ∀ 𝑦𝐴𝑧𝐵 𝜓 )