freq1

Description: Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997)

		Ref	Expression
	Assertion	freq1	$⊢ R = S \to (R Fr A \leftrightarrow S Fr A)$

Step	Hyp	Ref	Expression
1		breq	$⊢ R = S \to (z R y \leftrightarrow z S y)$
2	1	notbid	$⊢ R = S \to (\neg z R y \leftrightarrow \neg z S y)$
3	2	rexralbidv	$⊢ R = S \to (\exists y \in x \forall z \in x \neg z R y \leftrightarrow \exists y \in x \forall z \in x \neg z S y)$
4	3	imbi2d	$⊢ R = S \to (((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z S y))$
5	4	albidv	$⊢ R = S \to (\forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z S y))$
6		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)$
7		df-fr	$⊢ S Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z S y)$
8	5 6 7	3bitr4g	$⊢ R = S \to (R Fr A \leftrightarrow S Fr A)$

Metamath Proof Explorer