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

Metamath Proof Explorer

Theorem coss2cnvepres

Description: Special case of coss1cnvres . (Contributed by Peter Mazsa, 8-Jun-2020)

Ref Expression
Assertion coss2cnvepres ≀ ◡ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) }

Proof

Step Hyp Ref Expression
1 coss1cnvres ⊢ ≀ ◡ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 ◡ E 𝑥 ∧ 𝑣 ◡ E 𝑥 ) ) }
2 brcnvep ⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 ) )
3 2 elv ⊢ ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 )
4 brcnvep ⊢ ( 𝑣 ∈ V → ( 𝑣 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑣 ) )
5 4 elv ⊢ ( 𝑣 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑣 )
6 3 5 anbi12i ⊢ ( ( 𝑢 ◡ E 𝑥 ∧ 𝑣 ◡ E 𝑥 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) )
7 6 exbii ⊢ ( ∃ 𝑥 ( 𝑢 ◡ E 𝑥 ∧ 𝑣 ◡ E 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) )
8 7 anbi2i ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 ◡ E 𝑥 ∧ 𝑣 ◡ E 𝑥 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) )
9 8 opabbii ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑢 ◡ E 𝑥 ∧ 𝑣 ◡ E 𝑥 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) }
10 1 9 eqtri ⊢ ≀ ◡ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) ) }