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

Metamath Proof Explorer

Theorem elabgw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A . This is to elabg what sbievw2 is to sbievw . (Contributed by SN, 20-Apr-2024)

	Ref	Expression
Hypotheses	elabgw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	elabgw.2	⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
Assertion	elabgw	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		elabgw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		elabgw.2	⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
5	1	sbievw	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
6	4 5	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
7	3 2 6	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 ) )