This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 ↾ 𝐴 ) / ( 𝑅 ↾ 𝐴 ) ) ↔ ∃ 𝑢 ∈ 𝐴 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐵 = [ 𝑢 ] 𝑅 ) )