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 ⊢ Ⅎ y φ
ralxpf.2 ⊢ Ⅎ z φ
ralxpf.3 ⊢ Ⅎ x ψ
ralxpf.4 ⊢ x = y z → φ ↔ ψ
Assertion rexxpf ⊢ ∃ x ∈ A × B φ ↔ ∃ y ∈ A ∃ z ∈ B ψ

Proof

Step Hyp Ref Expression
1 ralxpf.1 ⊢ Ⅎ y φ
2 ralxpf.2 ⊢ Ⅎ z φ
3 ralxpf.3 ⊢ Ⅎ x ψ
4 ralxpf.4 ⊢ x = y z → φ ↔ ψ
5 1 nfn ⊢ Ⅎ y ¬ φ
6 2 nfn ⊢ Ⅎ z ¬ φ
7 3 nfn ⊢ Ⅎ x ¬ ψ
8 4 notbid ⊢ x = y z → ¬ φ ↔ ¬ ψ
9 5 6 7 8 ralxpf ⊢ ∀ x ∈ A × B ¬ φ ↔ ∀ y ∈ A ∀ z ∈ B ¬ ψ
10 ralnex ⊢ ∀ z ∈ B ¬ ψ ↔ ¬ ∃ z ∈ B ψ
11 10 ralbii ⊢ ∀ y ∈ A ∀ z ∈ B ¬ ψ ↔ ∀ y ∈ A ¬ ∃ z ∈ B ψ
12 9 11 bitri ⊢ ∀ x ∈ A × B ¬ φ ↔ ∀ y ∈ A ¬ ∃ z ∈ B ψ
13 12 notbii ⊢ ¬ ∀ x ∈ A × B ¬ φ ↔ ¬ ∀ y ∈ A ¬ ∃ z ∈ B ψ
14 dfrex2 ⊢ ∃ x ∈ A × B φ ↔ ¬ ∀ x ∈ A × B ¬ φ
15 dfrex2 ⊢ ∃ y ∈ A ∃ z ∈ B ψ ↔ ¬ ∀ y ∈ A ¬ ∃ z ∈ B ψ
16 13 14 15 3bitr4i ⊢ ∃ x ∈ A × B φ ↔ ∃ y ∈ A ∃ z ∈ B ψ