Theorem elab3gf

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

	Ref	Expression
Hypotheses	elab3gf.1	⊢ Ⅎ 𝑥 𝐴
	elab3gf.2	⊢ Ⅎ 𝑥 𝜓
	elab3gf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	elab3gf	⊢ ( ( 𝜓 → 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elab3gf.1	⊢ Ⅎ 𝑥 𝐴
2		elab3gf.2	⊢ Ⅎ 𝑥 𝜓
3		elab3gf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4	1 2 3	elabgf	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
5	4	ibi	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } → 𝜓 )
6		pm2.21	⊢ ( ¬ 𝜓 → ( 𝜓 → 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
7	5 6	impbid2	⊢ ( ¬ 𝜓 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
8	1 2 3	elabgf	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
9	7 8	ja	⊢ ( ( 𝜓 → 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )