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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
elabd2.eq ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∣ 𝜓 } )
elabd2.is ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion elabd2 ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 elabd2.ex ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 elabd2.eq ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∣ 𝜓 } )
3 elabd2.is ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4 2 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } ) )
5 elab6g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) )
6 4 5 sylan9bb ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ) )
7 elisset ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
8 3 pm5.74da ⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( 𝑥 = 𝐴 → 𝜒 ) ) )
9 8 albidv ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜒 ) ) )
10 19.23v ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜒 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜒 ) )
11 9 10 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜒 ) ) )
12 pm5.5 ⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝜒 ) ↔ 𝜒 ) )
13 11 12 sylan9bb ⊢ ( ( 𝜑 ∧ ∃ 𝑥 𝑥 = 𝐴 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜒 ) )
14 7 13 sylan2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜓 ) ↔ 𝜒 ) )
15 6 14 bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )
16 1 15 mpdan ⊢ ( 𝜑 → ( 𝐴 ∈ 𝐵 ↔ 𝜒 ) )