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

Metamath Proof Explorer

Theorem r19.12sn

Description: Special case of r19.12 where its converse holds. (Contributed by NM, 19-May-2008) (Revised by Mario Carneiro, 23-Apr-2015) (Revised by BJ, 18-Mar-2020)

Ref Expression
Assertion r19.12sn ⊢ A ∈ V → ∃ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∃ x ∈ A φ

Proof

Step Hyp Ref Expression
1 sbcralg ⊢ A ∈ V → [˙A / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B [˙A / x]˙ φ
2 rexsns ⊢ ∃ x ∈ A ∀ y ∈ B φ ↔ [˙A / x]˙ ∀ y ∈ B φ
3 rexsns ⊢ ∃ x ∈ A φ ↔ [˙A / x]˙ φ
4 3 ralbii ⊢ ∀ y ∈ B ∃ x ∈ A φ ↔ ∀ y ∈ B [˙A / x]˙ φ
5 1 2 4 3bitr4g ⊢ A ∈ V → ∃ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ∃ x ∈ A φ