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

Metamath Proof Explorer

Theorem elab2gw

Description: Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on x and A , which is not usually significant since B is usually a constant. (Contributed by SN, 16-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elabgw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		elabgw.2	⊢ ( 𝑦 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
3		elab2gw.3	⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
4	3	eleq2i	⊢ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
5	1 2	elabgw	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜒 ) )
6	4 5	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )