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

Metamath Proof Explorer

Theorem 2ralsng

Description: Substitution expressed in terms of two quantifications over singletons. (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses ralsng.1 ⊢ x = A → φ ↔ ψ
2ralsng.1 ⊢ y = B → ψ ↔ χ
Assertion 2ralsng ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A ∀ y ∈ B φ ↔ χ

Proof

Step Hyp Ref Expression
1 ralsng.1 ⊢ x = A → φ ↔ ψ
2 2ralsng.1 ⊢ y = B → ψ ↔ χ
3 1 ralbidv ⊢ x = A → ∀ y ∈ B φ ↔ ∀ y ∈ B ψ
4 3 ralsng ⊢ A ∈ V → ∀ x ∈ A ∀ y ∈ B φ ↔ ∀ y ∈ B ψ
5 2 ralsng ⊢ B ∈ W → ∀ y ∈ B ψ ↔ χ
6 4 5 sylan9bb ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ A ∀ y ∈ B φ ↔ χ