Metamath Proof Explorer

Theorem eldmqsres

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

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

Proof

Step Hyp Ref Expression
1 elqsg ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A / R ↾ A ↔ ∃ u ∈ dom ⁡ R ↾ A B = u R ↾ A
2 eldmres2 ⊢ u ∈ V → u ∈ dom ⁡ R ↾ A ↔ u ∈ A ∧ ∃ x x ∈ u R
3 2 elv ⊢ u ∈ dom ⁡ R ↾ A ↔ u ∈ A ∧ ∃ x x ∈ u R
4 3 anbi1i ⊢ u ∈ dom ⁡ R ↾ A ∧ B = u R ↾ A ↔ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R ↾ A
5 ecres2 ⊢ u ∈ A → u R ↾ A = u R
6 5 eqeq2d ⊢ u ∈ A → B = u R ↾ A ↔ B = u R
7 6 pm5.32i ⊢ u ∈ A ∧ B = u R ↾ A ↔ u ∈ A ∧ B = u R
8 7 anbi2i ⊢ ∃ x x ∈ u R ∧ u ∈ A ∧ B = u R ↾ A ↔ ∃ x x ∈ u R ∧ u ∈ A ∧ B = u R
9 an21 ⊢ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R ↾ A ↔ ∃ x x ∈ u R ∧ u ∈ A ∧ B = u R ↾ A
10 an12 ⊢ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R ↔ ∃ x x ∈ u R ∧ u ∈ A ∧ B = u R
11 8 9 10 3bitr4i ⊢ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R ↾ A ↔ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R
12 4 11 bitri ⊢ u ∈ dom ⁡ R ↾ A ∧ B = u R ↾ A ↔ u ∈ A ∧ ∃ x x ∈ u R ∧ B = u R
13 12 rexbii2 ⊢ ∃ u ∈ dom ⁡ R ↾ A B = u R ↾ A ↔ ∃ u ∈ A ∃ x x ∈ u R ∧ B = u R
14 1 13 bitrdi ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A / R ↾ A ↔ ∃ u ∈ A ∃ x x ∈ u R ∧ B = u R