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

Metamath Proof Explorer

Theorem rexxpf

Description: Version of rexxp with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 ⊢ Ⅎ 𝑦 𝜑
ralxpf.2 ⊢ Ⅎ 𝑧 𝜑
ralxpf.3 ⊢ Ⅎ 𝑥 𝜓
ralxpf.4 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion rexxpf ( ∃ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝜓 )

Proof

Step Hyp Ref Expression
1 ralxpf.1 ⊢ Ⅎ 𝑦 𝜑
2 ralxpf.2 ⊢ Ⅎ 𝑧 𝜑
3 ralxpf.3 ⊢ Ⅎ 𝑥 𝜓
4 ralxpf.4 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
5 1 nfn ⊢ Ⅎ 𝑦 ¬ 𝜑
6 2 nfn ⊢ Ⅎ 𝑧 ¬ 𝜑
7 3 nfn ⊢ Ⅎ 𝑥 ¬ 𝜓
8 4 notbid ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
9 5 6 7 8 ralxpf ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 )
10 ralnex ⊢ ( ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
11 10 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ¬ 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
12 9 11 bitri ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
13 12 notbii ⊢ ( ¬ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
14 dfrex2 ⊢ ( ∃ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ¬ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ¬ 𝜑 )
15 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ ∃ 𝑧 ∈ 𝐵 𝜓 )
16 13 14 15 3bitr4i ⊢ ( ∃ 𝑥 ∈ ( 𝐴 × 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝜓 )