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	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	brfvidRP	$$⊢\phi \to \left(A\mathrm{I}\left(R\right)B\leftrightarrow ARB\right)$$

Proof

Step	Hyp	Ref	Expression
1		brfvidRP.r	$$⊢\phi \to R\in \mathrm{V}$$
2		dfid6	$$⊢\mathrm{I}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{1\right\}}\left(r{\uparrow }_{r}n\right)\right)$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		snssi	$$⊢1\in {\mathbb{N}}_0\to \left\{1\right\}\subseteq {\mathbb{N}}_0$$
5	3 4	mp1i	$$⊢\phi \to \left\{1\right\}\subseteq {\mathbb{N}}_0$$
6	2 1 5	brmptiunrelexpd	$$⊢\phi \to \left(A\mathrm{I}\left(R\right)B\leftrightarrow \exists n\in \left\{1\right\}A\left(R{\uparrow }_{r}n\right)B\right)$$
7		oveq2	$$⊢n=1\to R{\uparrow }_{r}n=R{\uparrow }_{r}1$$
8	7	breqd	$$⊢n=1\to \left(A\left(R{\uparrow }_{r}n\right)B\leftrightarrow A\left(R{\uparrow }_{r}1\right)B\right)$$
9	8	rexsng	$$⊢1\in {\mathbb{N}}_0\to \left(\exists n\in \left\{1\right\}A\left(R{\uparrow }_{r}n\right)B\leftrightarrow A\left(R{\uparrow }_{r}1\right)B\right)$$
10	3 9	mp1i	$$⊢\phi \to \left(\exists n\in \left\{1\right\}A\left(R{\uparrow }_{r}n\right)B\leftrightarrow A\left(R{\uparrow }_{r}1\right)B\right)$$
11	1	relexp1d	$$⊢\phi \to R{\uparrow }_{r}1=R$$
12	11	breqd	$$⊢\phi \to \left(A\left(R{\uparrow }_{r}1\right)B\leftrightarrow ARB\right)$$
13	6 10 12	3bitrd	$$⊢\phi \to \left(A\mathrm{I}\left(R\right)B\leftrightarrow ARB\right)$$