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	1	elabg	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
3	2	ibi	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } → 𝜓 )
4		pm2.21	⊢ ( ¬ 𝜓 → ( 𝜓 → 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
5	3 4	impbid2	⊢ ( ¬ 𝜓 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
6	1	elabg	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
7	5 6	ja	⊢ ( ( 𝜓 → 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )