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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	elab3g	⊢ ( ( 𝜓 → 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elab3g.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		nfcv	⊢ Ⅎ 𝑥 𝐴
3		nfv	⊢ Ⅎ 𝑥 𝜓
4	2 3 1	elab3gf	⊢ ( ( 𝜓 → 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )