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

Metamath Proof Explorer

Theorem vtoclgf

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003) (Proof shortened by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	vtoclgf.1	⊢ Ⅎ 𝑥 𝐴
	vtoclgf.2	⊢ Ⅎ 𝑥 𝜓
	vtoclgf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtoclgf.4	⊢ 𝜑
Assertion	vtoclgf	⊢ ( 𝐴 ∈ 𝑉 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		vtoclgf.1	⊢ Ⅎ 𝑥 𝐴
2		vtoclgf.2	⊢ Ⅎ 𝑥 𝜓
3		vtoclgf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		vtoclgf.4	⊢ 𝜑
5		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
6	1	issetf	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
7	4 3	mpbii	⊢ ( 𝑥 = 𝐴 → 𝜓 )
8	2 7	exlimi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜓 )
9	6 8	sylbi	⊢ ( 𝐴 ∈ V → 𝜓 )
10	5 9	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝜓 )