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

Metamath Proof Explorer

Theorem rexiunxp

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

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

Proof

Step Hyp Ref Expression
1 ralxp.1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2 1 notbid ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 2 raliunxp ⊢ ( ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 )
4 ralnex ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
5 4 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
6 3 5 bitri ⊢ ( ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
7 6 notbii ⊢ ( ¬ ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
8 dfrex2 ⊢ ( ∃ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ¬ ∀ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) ¬ 𝜑 )
9 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
10 7 8 9 3bitr4i ⊢ ( ∃ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝜓 )