Theorem bnj1212

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1212.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
	bnj1212.2	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏 ) )
Assertion	bnj1212	⊢ ( 𝜃 → 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj1212.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
2		bnj1212.2	⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑥 ∈ 𝐵 ∧ 𝜏 ) )
3	1	ssrab3	⊢ 𝐵 ⊆ 𝐴
4	2	simp2bi	⊢ ( 𝜃 → 𝑥 ∈ 𝐵 )
5	3 4	bnj1213	⊢ ( 𝜃 → 𝑥 ∈ 𝐴 )