Theorem ssrel3

Description: Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019)

	Ref	Expression
Assertion	ssrel3	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssrel	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
2		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3		df-br	⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
4	2 3	imbi12i	⊢ ( ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
5	4	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
6	1 5	bitr4di	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) ) )