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 ) )