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

Metamath Proof Explorer

Theorem rsp3eq

Description: From a restricted universal statement over A , specialize to an arbitrary element class, cf. rsp3 . (Contributed by Peter Mazsa, 9-Feb-2026)

Ref Expression
Hypotheses rsp3.1 ⊢ Ⅎ 𝑥 𝐴
rsp3.2 ⊢ Ⅎ 𝑦 𝐴
rsp3.3 ⊢ Ⅎ 𝑦 𝜑
rsp3.4 ⊢ Ⅎ 𝑥 𝜓
rsp3.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion rsp3eq ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑦 = 𝐵 ∧ 𝐵 ∈ 𝐴 ) → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rsp3.1 ⊢ Ⅎ 𝑥 𝐴
2 rsp3.2 ⊢ Ⅎ 𝑦 𝐴
3 rsp3.3 ⊢ Ⅎ 𝑦 𝜑
4 rsp3.4 ⊢ Ⅎ 𝑥 𝜓
5 rsp3.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6 eqeltr ⊢ ( ( 𝑦 = 𝐵 ∧ 𝐵 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
7 1 2 3 4 5 rsp3 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑦 ∈ 𝐴 → 𝜓 ) )
8 6 7 syl5 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑦 = 𝐵 ∧ 𝐵 ∈ 𝐴 ) → 𝜓 ) )