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

Metamath Proof Explorer

Theorem elab

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of Quine p. 44. (Contributed by NM, 1-Aug-1994) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 5-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 elab.1 ⊢ A ∈ V
2 elab.2 ⊢ x = A → φ ↔ ψ
3 2 elabg ⊢ A ∈ V → A ∈ x | φ ↔ ψ
4 1 3 ax-mp ⊢ A ∈ x | φ ↔ ψ