rexnal3

Description: Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020)

		Ref	Expression
	Assertion	rexnal3	$⊢ \exists x \in A \exists y \in B \exists z \in C \neg φ \leftrightarrow \neg \forall x \in A \forall y \in B \forall z \in C φ$

Step	Hyp	Ref	Expression
1		rexnal	$⊢ \exists z \in C \neg φ \leftrightarrow \neg \forall z \in C φ$
2	1	2rexbii	$⊢ \exists x \in A \exists y \in B \exists z \in C \neg φ \leftrightarrow \exists x \in A \exists y \in B \neg \forall z \in C φ$
3		rexnal2	$⊢ \exists x \in A \exists y \in B \neg \forall z \in C φ \leftrightarrow \neg \forall x \in A \forall y \in B \forall z \in C φ$
4	2 3	bitri	$⊢ \exists x \in A \exists y \in B \exists z \in C \neg φ \leftrightarrow \neg \forall x \in A \forall y \in B \forall z \in C φ$

Metamath Proof Explorer