Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

	Ref	Expression
Assertion	idref	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq R\leftrightarrow \forall x\in AxRx$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(x\in A⟼⟨x,x⟩\right)=\left(x\in A⟼⟨x,x⟩\right)$$
2	1	fmpt	$$⊢\forall x\in A⟨x,x⟩\in R\leftrightarrow \left(x\in A⟼⟨x,x⟩\right):A⟶R$$
3		opex	$$⊢⟨x,x⟩\in \mathrm{V}$$
4	3 1	fnmpti	$$⊢\left(x\in A⟼⟨x,x⟩\right)FnA$$
5		df-f	$$⊢\left(x\in A⟼⟨x,x⟩\right):A⟶R\leftrightarrow \left(\left(x\in A⟼⟨x,x⟩\right)FnA\wedge \mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)\subseteq R\right)$$
6	4 5	mpbiran	$$⊢\left(x\in A⟼⟨x,x⟩\right):A⟶R\leftrightarrow \mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)\subseteq R$$
7	2 6	bitri	$$⊢\forall x\in A⟨x,x⟩\in R\leftrightarrow \mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)\subseteq R$$
8		df-br	$$⊢xRx\leftrightarrow ⟨x,x⟩\in R$$
9	8	ralbii	$$⊢\forall x\in AxRx\leftrightarrow \forall x\in A⟨x,x⟩\in R$$
10		mptresid	$$⊢{\mathrm{I}\upharpoonright }_A=\left(x\in A⟼x\right)$$
11		vex	$$⊢x\in \mathrm{V}$$
12	11	fnasrn	$$⊢\left(x\in A⟼x\right)=\mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)$$
13	10 12	eqtri	$$⊢{\mathrm{I}\upharpoonright }_A=\mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)$$
14	13	sseq1i	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq R\leftrightarrow \mathrm{ran}\left(x\in A⟼⟨x,x⟩\right)\subseteq R$$
15	7 9 14	3bitr4ri	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq R\leftrightarrow \forall x\in AxRx$$