elab3gf

Description: Membership in a class abstraction, with a weaker antecedent than elabgf . (Contributed by NM, 6-Sep-2011)

	Ref	Expression
Hypotheses	elab3gf.1	$⊢ \underline{Ⅎ} x A$
	elab3gf.2	$⊢ Ⅎ x ψ$
	elab3gf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	elab3gf	$⊢ (ψ \to A \in B) \to (A \in \{x \| φ\} \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		elab3gf.1	$⊢ \underline{Ⅎ} x A$
2		elab3gf.2	$⊢ Ⅎ x ψ$
3		elab3gf.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
4	1 2 3	elabgf	$⊢ A \in \{x \| φ\} \to (A \in \{x \| φ\} \leftrightarrow ψ)$
5	4	ibi	$⊢ A \in \{x \| φ\} \to ψ$
6		pm2.21	$⊢ \neg ψ \to (ψ \to A \in \{x \| φ\})$
7	5 6	impbid2	$⊢ \neg ψ \to (A \in \{x \| φ\} \leftrightarrow ψ)$
8	1 2 3	elabgf	$⊢ A \in B \to (A \in \{x \| φ\} \leftrightarrow ψ)$
9	7 8	ja	$⊢ (ψ \to A \in B) \to (A \in \{x \| φ\} \leftrightarrow ψ)$

Metamath Proof Explorer