This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indifbi

Description: Two ways to express equality relative to a class A . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion indifbi 
|- ( ( A i^i B ) = ( A i^i C ) <-> ( A \ B ) = ( A \ C ) )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( A i^i B ) C_ A
2 inss1 
 |-  ( A i^i C ) C_ A
3 rcompleq 
 |-  ( ( ( A i^i B ) C_ A /\ ( A i^i C ) C_ A ) -> ( ( A i^i B ) = ( A i^i C ) <-> ( A \ ( A i^i B ) ) = ( A \ ( A i^i C ) ) ) )
4 1 2 3 mp2an 
 |-  ( ( A i^i B ) = ( A i^i C ) <-> ( A \ ( A i^i B ) ) = ( A \ ( A i^i C ) ) )
5 difin 
 |-  ( A \ ( A i^i B ) ) = ( A \ B )
6 difin 
 |-  ( A \ ( A i^i C ) ) = ( A \ C )
7 5 6 eqeq12i 
 |-  ( ( A \ ( A i^i B ) ) = ( A \ ( A i^i C ) ) <-> ( A \ B ) = ( A \ C ) )
8 4 7 bitri 
 |-  ( ( A i^i B ) = ( A i^i C ) <-> ( A \ B ) = ( A \ C ) )