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 ⊢ x = y → φ ↔ ψ
elabgw.2 ⊢ y = A → ψ ↔ χ
Assertion elabgw ⊢ A ∈ V → A ∈ x | φ ↔ χ

Proof

Step Hyp Ref Expression
1 elabgw.1 ⊢ x = y → φ ↔ ψ
2 elabgw.2 ⊢ y = A → ψ ↔ χ
3 eleq1 ⊢ y = A → y ∈ x | φ ↔ A ∈ x | φ
4 df-clab ⊢ y ∈ x | φ ↔ y x φ
5 1 sbievw ⊢ y x φ ↔ ψ
6 4 5 bitri ⊢ y ∈ x | φ ↔ ψ
7 3 2 6 vtoclbg ⊢ A ∈ V → A ∈ x | φ ↔ χ