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

Metamath Proof Explorer

Theorem ralsng

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015) Avoid ax-10 , ax-12 . (Revised by GG, 30-Sep-2024)

Ref Expression
Hypothesis ralsng.1 ⊢ x = A → φ ↔ ψ
Assertion ralsng ⊢ A ∈ V → ∀ x ∈ A φ ↔ ψ

Proof

Step Hyp Ref Expression
1 ralsng.1 ⊢ x = A → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
3 velsn ⊢ x ∈ A ↔ x = A
4 3 imbi1i ⊢ x ∈ A → φ ↔ x = A → φ
5 4 albii ⊢ ∀ x x ∈ A → φ ↔ ∀ x x = A → φ
6 2 5 bitri ⊢ ∀ x ∈ A φ ↔ ∀ x x = A → φ
7 elisset ⊢ A ∈ V → ∃ x x = A
8 1 pm5.74i ⊢ x = A → φ ↔ x = A → ψ
9 8 albii ⊢ ∀ x x = A → φ ↔ ∀ x x = A → ψ
10 9 a1i ⊢ ∃ x x = A → ∀ x x = A → φ ↔ ∀ x x = A → ψ
11 19.23v ⊢ ∀ x x = A → ψ ↔ ∃ x x = A → ψ
12 11 a1i ⊢ ∃ x x = A → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
13 pm5.5 ⊢ ∃ x x = A → ∃ x x = A → ψ ↔ ψ
14 10 12 13 3bitrd ⊢ ∃ x x = A → ∀ x x = A → φ ↔ ψ
15 7 14 syl ⊢ A ∈ V → ∀ x x = A → φ ↔ ψ
16 6 15 bitrid ⊢ A ∈ V → ∀ x ∈ A φ ↔ ψ