Metamath Proof Explorer

Theorem elabd2

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

Ref Expression
Hypotheses elabd2.1 ⊢ φ → A ∈ V
elabd2.2 ⊢ φ ∧ x = A → ψ ↔ χ
Assertion elabd2 ⊢ φ → A ∈ x | ψ ↔ χ

Proof

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