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