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	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	brfvidRP	⊢ ( 𝜑 → ( 𝐴 ( I ‘ 𝑅 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brfvidRP.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dfid6	⊢ I = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 1 } ( 𝑟 ↑𝑟 𝑛 ) )
3		1nn0	⊢ 1 ∈ ℕ0
4		snssi	⊢ ( 1 ∈ ℕ0 → { 1 } ⊆ ℕ0 )
5	3 4	mp1i	⊢ ( 𝜑 → { 1 } ⊆ ℕ0 )
6	2 1 5	brmptiunrelexpd	⊢ ( 𝜑 → ( 𝐴 ( I ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ { 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
7		oveq2	⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
8	7	breqd	⊢ ( 𝑛 = 1 → ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) )
9	8	rexsng	⊢ ( 1 ∈ ℕ0 → ( ∃ 𝑛 ∈ { 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) )
10	3 9	mp1i	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ { 1 } 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ) )
11	1	relexp1d	⊢ ( 𝜑 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
12	11	breqd	⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ↑𝑟 1 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )
13	6 10 12	3bitrd	⊢ ( 𝜑 → ( 𝐴 ( I ‘ 𝑅 ) 𝐵 ↔ 𝐴 𝑅 𝐵 ) )