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

Metamath Proof Explorer

Theorem elabd2

Description: Membership in a class abstraction, using implicit substitution. Deduction version of elab . (Contributed by GG, 12-Oct-2024) (Revised by BJ, 16-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 elabd2.ex ⊢ φ → A ∈ V
2 elabd2.eq ⊢ φ → B = x | ψ
3 elabd2.is ⊢ φ ∧ x = A → ψ ↔ χ
4 2 eleq2d ⊢ φ → A ∈ B ↔ A ∈ x | ψ
5 elab6g ⊢ A ∈ V → A ∈ x | ψ ↔ ∀ x x = A → ψ
6 4 5 sylan9bb ⊢ φ ∧ A ∈ V → A ∈ B ↔ ∀ x x = A → ψ
7 elisset ⊢ A ∈ V → ∃ x x = A
8 3 pm5.74da ⊢ φ → x = A → ψ ↔ x = A → χ
9 8 albidv ⊢ φ → ∀ x x = A → ψ ↔ ∀ x x = A → χ
10 19.23v ⊢ ∀ x x = A → χ ↔ ∃ x x = A → χ
11 9 10 bitrdi ⊢ φ → ∀ x x = A → ψ ↔ ∃ x x = A → χ
12 pm5.5 ⊢ ∃ x x = A → ∃ x x = A → χ ↔ χ
13 11 12 sylan9bb ⊢ φ ∧ ∃ x x = A → ∀ x x = A → ψ ↔ χ
14 7 13 sylan2 ⊢ φ ∧ A ∈ V → ∀ x x = A → ψ ↔ χ
15 6 14 bitrd ⊢ φ ∧ A ∈ V → A ∈ B ↔ χ
16 1 15 mpdan ⊢ φ → A ∈ B ↔ χ