rexsupp

Description: Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by AV, 27-May-2019)

		Ref	Expression
	Assertion	rexsupp	$⊢ (F Fn X \land X \in V \land Z \in W) \to (\exists x \in {supp}_{Z} (F) φ \leftrightarrow \exists x \in X (F (x) \neq Z \land φ))$

Step	Hyp	Ref	Expression
1		elsuppfn	$⊢ (F Fn X \land X \in V \land Z \in W) \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in X \land F (x) \neq Z))$
2	1	anbi1d	$⊢ (F Fn X \land X \in V \land Z \in W) \to ((x \in {supp}_{Z} (F) \land φ) \leftrightarrow ((x \in X \land F (x) \neq Z) \land φ))$
3		anass	$⊢ ((x \in X \land F (x) \neq Z) \land φ) \leftrightarrow (x \in X \land (F (x) \neq Z \land φ))$
4	2 3	bitrdi	$⊢ (F Fn X \land X \in V \land Z \in W) \to ((x \in {supp}_{Z} (F) \land φ) \leftrightarrow (x \in X \land (F (x) \neq Z \land φ)))$
5	4	rexbidv2	$⊢ (F Fn X \land X \in V \land Z \in W) \to (\exists x \in {supp}_{Z} (F) φ \leftrightarrow \exists x \in X (F (x) \neq Z \land φ))$

Metamath Proof Explorer