Theorem brfvidRP

Description: If two elements are connected by a value of the identity relation, then they are connected via the argument. This is an example which uses brmptiunrelexpd . (Contributed by RP, 21-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	brfvidRP.r	|- ( ph -> R e. _V )
Assertion	brfvidRP	|- ( ph -> ( A ( _I ` R ) B <-> A R B ) )

Proof

Step	Hyp	Ref	Expression
1		brfvidRP.r	|- ( ph -> R e. _V )
2		dfid6	|- _I = ( r e. _V |-> U_ n e. { 1 } ( r ^r n ) )
3		1nn0	|- 1 e. NN0
4		snssi	|- ( 1 e. NN0 -> { 1 } C_ NN0 )
5	3 4	mp1i	|- ( ph -> { 1 } C_ NN0 )
6	2 1 5	brmptiunrelexpd	|- ( ph -> ( A ( _I ` R ) B <-> E. n e. { 1 } A ( R ^r n ) B ) )
7		oveq2	|- ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
8	7	breqd	|- ( n = 1 -> ( A ( R ^r n ) B <-> A ( R ^r 1 ) B ) )
9	8	rexsng	|- ( 1 e. NN0 -> ( E. n e. { 1 } A ( R ^r n ) B <-> A ( R ^r 1 ) B ) )
10	3 9	mp1i	|- ( ph -> ( E. n e. { 1 } A ( R ^r n ) B <-> A ( R ^r 1 ) B ) )
11	1	relexp1d	|- ( ph -> ( R ^r 1 ) = R )
12	11	breqd	|- ( ph -> ( A ( R ^r 1 ) B <-> A R B ) )
13	6 10 12	3bitrd	|- ( ph -> ( A ( _I ` R ) B <-> A R B ) )