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

Metamath Proof Explorer

Theorem vtoclri

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994)

Ref Expression
Hypotheses vtoclri.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
vtoclri.2 ⊢ ∀ 𝑥 ∈ 𝐵 𝜑
Assertion vtoclri ( 𝐴 ∈ 𝐵 → 𝜓 )

Proof

Step Hyp Ref Expression
1 vtoclri.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 vtoclri.2 ⊢ ∀ 𝑥 ∈ 𝐵 𝜑
3 2 rspec ⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
4 1 3 vtoclga ⊢ ( 𝐴 ∈ 𝐵 → 𝜓 )