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