Metamath Proof Explorer


Theorem eldm1cossres

Description: Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018)

Ref Expression
Assertion eldm1cossres ( 𝐵𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅𝐴 ) ↔ ∃ 𝑢𝐴 𝑢 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eldmcoss ( 𝐵𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅𝐴 ) ↔ ∃ 𝑢 𝑢 ( 𝑅𝐴 ) 𝐵 ) )
2 brres ( 𝐵𝑉 → ( 𝑢 ( 𝑅𝐴 ) 𝐵 ↔ ( 𝑢𝐴𝑢 𝑅 𝐵 ) ) )
3 2 exbidv ( 𝐵𝑉 → ( ∃ 𝑢 𝑢 ( 𝑅𝐴 ) 𝐵 ↔ ∃ 𝑢 ( 𝑢𝐴𝑢 𝑅 𝐵 ) ) )
4 1 3 bitrd ( 𝐵𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅𝐴 ) ↔ ∃ 𝑢 ( 𝑢𝐴𝑢 𝑅 𝐵 ) ) )
5 df-rex ( ∃ 𝑢𝐴 𝑢 𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢𝐴𝑢 𝑅 𝐵 ) )
6 4 5 bitr4di ( 𝐵𝑉 → ( 𝐵 ∈ dom ≀ ( 𝑅𝐴 ) ↔ ∃ 𝑢𝐴 𝑢 𝑅 𝐵 ) )