Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Additional statements on relations and subclasses
Finite relationship composition.
brfvid
Metamath Proof Explorer
Description: If two elements are connected by a value of the identity relation, then
they are connected via the argument. (Contributed by RP , 21-Jul-2020)
Ref
Expression
Hypothesis
brfvid.r
⊢ φ → R ∈ V
Assertion
brfvid
⊢ φ → A I ⁡ R B ↔ A R B
Proof
Step
Hyp
Ref
Expression
1
brfvid.r
⊢ φ → R ∈ V
2
fvi
⊢ R ∈ V → I ⁡ R = R
3
1 2
syl
⊢ φ → I ⁡ R = R
4
3
breqd
⊢ φ → A I ⁡ R B ↔ A R B