Theorem rabeqel

Description: Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021)

	Ref	Expression
Hypotheses	rabeqel.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
	rabeqel.2	⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rabeqel	⊢ ( 𝐶 ∈ 𝐵 ↔ ( 𝜓 ∧ 𝐶 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rabeqel.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
2		rabeqel.2	⊢ ( 𝑥 = 𝐶 → ( 𝜑 ↔ 𝜓 ) )
3	2 1	elrab2	⊢ ( 𝐶 ∈ 𝐵 ↔ ( 𝐶 ∈ 𝐴 ∧ 𝜓 ) )
4	3	biancomi	⊢ ( 𝐶 ∈ 𝐵 ↔ ( 𝜓 ∧ 𝐶 ∈ 𝐴 ) )