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 ⊢ B = x ∈ A | φ
rabeqel.2 ⊢ x = C → φ ↔ ψ
Assertion rabeqel ⊢ C ∈ B ↔ ψ ∧ C ∈ A

Proof

Step Hyp Ref Expression
1 rabeqel.1 ⊢ B = x ∈ A | φ
2 rabeqel.2 ⊢ x = C → φ ↔ ψ
3 2 1 elrab2 ⊢ C ∈ B ↔ C ∈ A ∧ ψ
4 3 biancomi ⊢ C ∈ B ↔ ψ ∧ C ∈ A