dffr2ALT

Description: Alternate proof of dffr2 , which avoids ax-8 but requires ax-10 , ax-11 , ax-12 . (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	dffr2ALT	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		df-fr	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
2		rabeq0	$⊢ \{z \in x \| z R y\} = \emptyset \leftrightarrow \forall z \in x \neg z R y$
3	2	rexbii	$⊢ \exists y \in x \{z \in x \| z R y\} = \emptyset \leftrightarrow \exists y \in x \forall z \in x \neg z R y$
4	3	imbi2i	$⊢ ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
5	4	albii	$⊢ \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
6	1 5	bitr4i	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$

Metamath Proof Explorer

Theorem dffr2ALT

Proof