Metamath Proof Explorer


Theorem eldmqsres2

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

Ref Expression
Assertion eldmqsres2 ( 𝐵𝑉 → ( 𝐵 ∈ ( dom ( 𝑅𝐴 ) / ( 𝑅𝐴 ) ) ↔ ∃ 𝑢𝐴𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eldmqsres ( 𝐵𝑉 → ( 𝐵 ∈ ( dom ( 𝑅𝐴 ) / ( 𝑅𝐴 ) ) ↔ ∃ 𝑢𝐴 ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) ) )
2 df-rex ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) )
3 19.41v ( ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) )
4 2 3 bitri ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) )
5 4 rexbii ( ∃ 𝑢𝐴𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ↔ ∃ 𝑢𝐴 ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅𝐵 = [ 𝑢 ] 𝑅 ) )
6 1 5 bitr4di ( 𝐵𝑉 → ( 𝐵 ∈ ( dom ( 𝑅𝐴 ) / ( 𝑅𝐴 ) ) ↔ ∃ 𝑢𝐴𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ) )