This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐶 ∈ 𝐵 ↔ ( 𝜓 ∧ 𝐶 ∈ 𝐴 ) )