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

Metamath Proof Explorer

Theorem ralsngf

Description: Restricted universal quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by AV, 3-Apr-2023)

Ref Expression
Hypotheses rexsngf.1 ⊢ Ⅎ 𝑥 𝜓
rexsngf.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion ralsngf ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rexsngf.1 ⊢ Ⅎ 𝑥 𝜓
2 rexsngf.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 ralsnsg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
4 1 2 sbciegf ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
5 3 4 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) )