Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
eqrel2
Next ⟩
rncnv
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqrel2
Description:
Equality of relations.
(Contributed by
Peter Mazsa
, 8-Mar-2019)
Ref
Expression
Assertion
eqrel2
⊢
Rel
⁡
A
∧
Rel
⁡
B
→
A
=
B
↔
∀
x
∀
y
x
A
y
↔
x
B
y
Proof
Step
Hyp
Ref
Expression
1
ssrel3
⊢
Rel
⁡
A
→
A
⊆
B
↔
∀
x
∀
y
x
A
y
→
x
B
y
2
ssrel3
⊢
Rel
⁡
B
→
B
⊆
A
↔
∀
x
∀
y
x
B
y
→
x
A
y
3
1
2
bi2anan9
⊢
Rel
⁡
A
∧
Rel
⁡
B
→
A
⊆
B
∧
B
⊆
A
↔
∀
x
∀
y
x
A
y
→
x
B
y
∧
∀
x
∀
y
x
B
y
→
x
A
y
4
eqss
⊢
A
=
B
↔
A
⊆
B
∧
B
⊆
A
5
2albiim
⊢
∀
x
∀
y
x
A
y
↔
x
B
y
↔
∀
x
∀
y
x
A
y
→
x
B
y
∧
∀
x
∀
y
x
B
y
→
x
A
y
6
3
4
5
3bitr4g
⊢
Rel
⁡
A
∧
Rel
⁡
B
→
A
=
B
↔
∀
x
∀
y
x
A
y
↔
x
B
y