Metamath Proof Explorer

Theorem bj-elabd2ALT

Description: Alternate proof of elabd2 bypassing elab6g (and using sbiedvw instead of the A. x ( x = y -> ps ) idiom). (Contributed by BJ, 16-Oct-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses bj-elabd2ALT.ex ⊢ φ → A ∈ V
bj-elabd2ALT.eq ⊢ φ → B = x | ψ
bj-elabd2ALT.is ⊢ φ ∧ x = A → ψ ↔ χ
Assertion bj-elabd2ALT ⊢ φ → A ∈ B ↔ χ

Proof

Step Hyp Ref Expression
1 bj-elabd2ALT.ex ⊢ φ → A ∈ V
2 bj-elabd2ALT.eq ⊢ φ → B = x | ψ
3 bj-elabd2ALT.is ⊢ φ ∧ x = A → ψ ↔ χ
4 simpr ⊢ φ ∧ y = A → y = A
5 2 eqcomd ⊢ φ → x | ψ = B
6 5 adantr ⊢ φ ∧ y = A → x | ψ = B
7 4 6 eleq12d ⊢ φ ∧ y = A → y ∈ x | ψ ↔ A ∈ B
8 eqeq1 ⊢ x = y → x = A ↔ y = A
9 8 biimparc ⊢ y = A ∧ x = y → x = A
10 9 anim2i ⊢ φ ∧ y = A ∧ x = y → φ ∧ x = A
11 10 anassrs ⊢ φ ∧ y = A ∧ x = y → φ ∧ x = A
12 11 3 syl ⊢ φ ∧ y = A ∧ x = y → ψ ↔ χ
13 12 sbiedvw ⊢ φ ∧ y = A → y x ψ ↔ χ
14 7 13 bibi12d ⊢ φ ∧ y = A → y ∈ x | ψ ↔ y x ψ ↔ A ∈ B ↔ χ
15 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
16 15 a1i ⊢ φ → y ∈ x | ψ ↔ y x ψ
17 1 14 16 vtocld ⊢ φ → A ∈ B ↔ χ