Metamath Proof Explorer

Theorem eldmqsres2

Description: Elementhood in a restricted domain quotient set. (Contributed by Peter Mazsa, 22-Aug-2020)

Ref Expression
Assertion eldmqsres2 ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A / R ↾ A ↔ ∃ u ∈ A ∃ x ∈ u R B = u R

Proof

Step Hyp Ref Expression
1 eldmqsres ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A / R ↾ A ↔ ∃ u ∈ A ∃ x x ∈ u R ∧ B = u R
2 df-rex ⊢ ∃ x ∈ u R B = u R ↔ ∃ x x ∈ u R ∧ B = u R
3 19.41v ⊢ ∃ x x ∈ u R ∧ B = u R ↔ ∃ x x ∈ u R ∧ B = u R
4 2 3 bitri ⊢ ∃ x ∈ u R B = u R ↔ ∃ x x ∈ u R ∧ B = u R
5 4 rexbii ⊢ ∃ u ∈ A ∃ x ∈ u R B = u R ↔ ∃ u ∈ A ∃ x x ∈ u R ∧ B = u R
6 1 5 bitr4di ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A / R ↾ A ↔ ∃ u ∈ A ∃ x ∈ u R B = u R