Metamath Proof Explorer


Theorem relssdmrnOLD

Description: Obsolete version of relssdmrn as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion relssdmrnOLD ( Rel 𝐴𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )

Proof

Step Hyp Ref Expression
1 id ( Rel 𝐴 → Rel 𝐴 )
2 19.8a ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3 19.8a ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ∃ 𝑥𝑥 , 𝑦 ⟩ ∈ 𝐴 )
4 opelxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴𝑦 ∈ ran 𝐴 ) )
5 vex 𝑥 ∈ V
6 5 eldm2 ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐴 )
7 vex 𝑦 ∈ V
8 7 elrn2 ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥𝑥 , 𝑦 ⟩ ∈ 𝐴 )
9 6 8 anbi12i ( ( 𝑥 ∈ dom 𝐴𝑦 ∈ ran 𝐴 ) ↔ ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑥𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
10 4 9 bitri ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ↔ ( ∃ 𝑦𝑥 , 𝑦 ⟩ ∈ 𝐴 ∧ ∃ 𝑥𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
11 2 3 10 sylanbrc ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) )
12 11 a1i ( Rel 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( dom 𝐴 × ran 𝐴 ) ) )
13 1 12 relssdv ( Rel 𝐴𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )