Theorem friOLD

Description: Obsolete version of fri as of 16-Nov-2024. (Contributed by NM, 18-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	friOLD	$$⊢\left(\left(B\in C\wedge R\mathrm{Fr}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists x\in B\forall y\in B\neg yRx$$

Proof

Step	Hyp	Ref	Expression
1		df-fr	$$⊢R\mathrm{Fr}A\leftrightarrow \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)$$
2		sseq1	$$⊢z=B\to \left(z\subseteq A\leftrightarrow B\subseteq A\right)$$
3		neeq1	$$⊢z=B\to \left(z\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
4	2 3	anbi12d	$$⊢z=B\to \left(\left(z\subseteq A\wedge z\ne \varnothing \right)\leftrightarrow \left(B\subseteq A\wedge B\ne \varnothing \right)\right)$$
5		raleq	$$⊢z=B\to \left(\forall y\in z\neg yRx\leftrightarrow \forall y\in B\neg yRx\right)$$
6	5	rexeqbi1dv	$$⊢z=B\to \left(\exists x\in z\forall y\in z\neg yRx\leftrightarrow \exists x\in B\forall y\in B\neg yRx\right)$$
7	4 6	imbi12d	$$⊢z=B\to \left(\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)\leftrightarrow \left(\left(B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\forall y\in B\neg yRx\right)\right)$$
8	7	spcgv	$$⊢B\in C\to \left(\forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)\to \left(\left(B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\forall y\in B\neg yRx\right)\right)$$
9	1 8	biimtrid	$$⊢B\in C\to \left(R\mathrm{Fr}A\to \left(\left(B\subseteq A\wedge B\ne \varnothing \right)\to \exists x\in B\forall y\in B\neg yRx\right)\right)$$
10	9	imp31	$$⊢\left(\left(B\in C\wedge R\mathrm{Fr}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists x\in B\forall y\in B\neg yRx$$