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

Metamath Proof Explorer

Theorem ralsnsg

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion ralsnsg ⊢ A ∈ V → ∀ x ∈ A φ ↔ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
2 velsn ⊢ x ∈ A ↔ x = A
3 2 imbi1i ⊢ x ∈ A → φ ↔ x = A → φ
4 3 albii ⊢ ∀ x x ∈ A → φ ↔ ∀ x x = A → φ
5 1 4 bitri ⊢ ∀ x ∈ A φ ↔ ∀ x x = A → φ
6 sbc6g ⊢ A ∈ V → [˙A / x]˙ φ ↔ ∀ x x = A → φ
7 5 6 bitr4id ⊢ A ∈ V → ∀ x ∈ A φ ↔ [˙A / x]˙ φ