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

Metamath Proof Explorer

Theorem elab2

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995)

Ref Expression
Hypotheses elab2.1 ⊢ 𝐴 ∈ V
elab2.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
elab2.3 ⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
Assertion elab2 ( 𝐴 ∈ 𝐵 ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 elab2.1 ⊢ 𝐴 ∈ V
2 elab2.2 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 elab2.3 ⊢ 𝐵 = { 𝑥 ∣ 𝜑 }
4 2 3 elab2g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝐵 ↔ 𝜓 ) )
5 1 4 ax-mp ⊢ ( 𝐴 ∈ 𝐵 ↔ 𝜓 )