Metamath Proof Explorer

Theorem eldmqs1cossres

Description: Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019)

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

Proof

Step Hyp Ref Expression
1 elqsg ⊢B∈V→B∈dom⁡≀R↾A/≀R↾A↔∃x∈dom⁡≀R↾AB=x≀R↾A
2 df-rex ⊢∃x∈dom⁡≀R↾AB=x≀R↾A↔∃xx∈dom⁡≀R↾A∧B=x≀R↾A
3 eldm1cossres2 ⊢x∈V→x∈dom⁡≀R↾A↔∃u∈Ax∈uR
4 3 elv ⊢x∈dom⁡≀R↾A↔∃u∈Ax∈uR
5 4 anbi1i ⊢x∈dom⁡≀R↾A∧B=x≀R↾A↔∃u∈Ax∈uR∧B=x≀R↾A
6 5 exbii ⊢∃xx∈dom⁡≀R↾A∧B=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
7 2 6 bitri ⊢∃x∈dom⁡≀R↾AB=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
8 1 7 bitrdi ⊢B∈V→B∈dom⁡≀R↾A/≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
9 df-rex ⊢∃x∈uRB=x≀R↾A↔∃xx∈uR∧B=x≀R↾A
10 9 rexbii ⊢∃u∈A∃x∈uRB=x≀R↾A↔∃u∈A∃xx∈uR∧B=x≀R↾A
11 rexcom4 ⊢∃u∈A∃xx∈uR∧B=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
12 r19.41v ⊢∃u∈Ax∈uR∧B=x≀R↾A↔∃u∈Ax∈uR∧B=x≀R↾A
13 12 exbii ⊢∃x∃u∈Ax∈uR∧B=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
14 11 13 bitri ⊢∃u∈A∃xx∈uR∧B=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
15 10 14 bitri ⊢∃u∈A∃x∈uRB=x≀R↾A↔∃x∃u∈Ax∈uR∧B=x≀R↾A
16 8 15 bitr4di ⊢B∈V→B∈dom⁡≀R↾A/≀R↾A↔∃u∈A∃x∈uRB=x≀R↾A