Metamath Proof Explorer


Theorem elabd3

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

Ref Expression
Hypotheses elabd3.ex ( 𝜑𝐴𝑉 )
elabd3.is ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
Assertion elabd3 ( 𝜑 → ( 𝐴 ∈ { 𝑥𝜓 } ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 elabd3.ex ( 𝜑𝐴𝑉 )
2 elabd3.is ( ( 𝜑𝑥 = 𝐴 ) → ( 𝜓𝜒 ) )
3 eqidd ( 𝜑 → { 𝑥𝜓 } = { 𝑥𝜓 } )
4 1 3 2 elabd2 ( 𝜑 → ( 𝐴 ∈ { 𝑥𝜓 } ↔ 𝜒 ) )