Theorem bj-vtoclgfALT

Description: Alternate proof of vtoclgf . Proof from vtoclgft . (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		bj-vtoclgfALT.1	⊢ Ⅎ 𝑥 𝐴
2		bj-vtoclgfALT.2	⊢ Ⅎ 𝑥 𝜓
3		bj-vtoclgfALT.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		bj-vtoclgfALT.4	⊢ 𝜑
5	1 2	pm3.2i	⊢ ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 )
6	3	ax-gen	⊢ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
7	4	ax-gen	⊢ ∀ 𝑥 𝜑
8	6 7	pm3.2i	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 𝜑 )
9		vtoclgft	⊢ ( ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝜓 ) ∧ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 𝜑 ) ∧ 𝐴 ∈ 𝑉 ) → 𝜓 )
10	5 8 9	mp3an12	⊢ ( 𝐴 ∈ 𝑉 → 𝜓 )