Metamath Proof Explorer


Theorem frege114d

Description: If either R relates A and B or A and B are the same, then either A and B are the same, R relates A and B , R relates B and A . Similar to Proposition 114 of Frege1879 p. 76. Compare with frege114 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypothesis frege114d.ab ( 𝜑 → ( 𝐴 𝑅 𝐵𝐴 = 𝐵 ) )
Assertion frege114d ( 𝜑 → ( 𝐴 𝑅 𝐵𝐴 = 𝐵𝐵 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 frege114d.ab ( 𝜑 → ( 𝐴 𝑅 𝐵𝐴 = 𝐵 ) )
2 df-3or ( ( 𝐴 𝑅 𝐵𝐴 = 𝐵𝐵 𝑅 𝐴 ) ↔ ( ( 𝐴 𝑅 𝐵𝐴 = 𝐵 ) ∨ 𝐵 𝑅 𝐴 ) )
3 2 biimpri ( ( ( 𝐴 𝑅 𝐵𝐴 = 𝐵 ) ∨ 𝐵 𝑅 𝐴 ) → ( 𝐴 𝑅 𝐵𝐴 = 𝐵𝐵 𝑅 𝐴 ) )
4 3 orcs ( ( 𝐴 𝑅 𝐵𝐴 = 𝐵 ) → ( 𝐴 𝑅 𝐵𝐴 = 𝐵𝐵 𝑅 𝐴 ) )
5 1 4 syl ( 𝜑 → ( 𝐴 𝑅 𝐵𝐴 = 𝐵𝐵 𝑅 𝐴 ) )