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

Metamath Proof Explorer

Theorem elab3g

Description: Membership in a class abstraction, with a weaker antecedent than elabg . (Contributed by NM, 29-Aug-2006)

Ref Expression
Hypothesis elab3g.1 ⊢ x = A → φ ↔ ψ
Assertion elab3g ⊢ ψ → A ∈ B → A ∈ x | φ ↔ ψ

Proof

Step Hyp Ref Expression
1 elab3g.1 ⊢ x = A → φ ↔ ψ
2 1 elabg ⊢ A ∈ x | φ → A ∈ x | φ ↔ ψ
3 2 ibi ⊢ A ∈ x | φ → ψ
4 pm2.21 ⊢ ¬ ψ → ψ → A ∈ x | φ
5 3 4 impbid2 ⊢ ¬ ψ → A ∈ x | φ ↔ ψ
6 1 elabg ⊢ A ∈ B → A ∈ x | φ ↔ ψ
7 5 6 ja ⊢ ψ → A ∈ B → A ∈ x | φ ↔ ψ