exdistrf

Description: Distribution of existential quantifiers, with a bound-variable hypothesis saying that y is not free in ph , but x can be free in ph (and there is no distinct variable condition on x and y ). (Contributed by Mario Carneiro, 20-Mar-2013) (Proof shortened by Wolf Lammen, 14-May-2018) Usage of this theorem is discouraged because it depends on ax-13 . Use exdistr instead. (New usage is discouraged.)

		Ref	Expression
	Hypothesis	exdistrf.1	$⊢ \neg \forall x x = y \to Ⅎ y φ$
	Assertion	exdistrf	$⊢ \exists x \exists y (φ \land ψ) \to \exists x (φ \land \exists y ψ)$

Proof

Step	Hyp	Ref	Expression
1		exdistrf.1	$⊢ \neg \forall x x = y \to Ⅎ y φ$
2		nfe1	$⊢ Ⅎ x \exists x (φ \land \exists y ψ)$
3		19.8a	$⊢ ψ \to \exists y ψ$
4	3	anim2i	$⊢ (φ \land ψ) \to (φ \land \exists y ψ)$
5	4	eximi	$⊢ \exists y (φ \land ψ) \to \exists y (φ \land \exists y ψ)$
6		biidd	$⊢ \forall x x = y \to ((φ \land \exists y ψ) \leftrightarrow (φ \land \exists y ψ))$
7	6	drex1	$⊢ \forall x x = y \to (\exists x (φ \land \exists y ψ) \leftrightarrow \exists y (φ \land \exists y ψ))$
8	5 7	imbitrrid	$⊢ \forall x x = y \to (\exists y (φ \land ψ) \to \exists x (φ \land \exists y ψ))$
9		19.40	$⊢ \exists y (φ \land ψ) \to (\exists y φ \land \exists y ψ)$
10	1	19.9d	$⊢ \neg \forall x x = y \to (\exists y φ \to φ)$
11	10	anim1d	$⊢ \neg \forall x x = y \to ((\exists y φ \land \exists y ψ) \to (φ \land \exists y ψ))$
12		19.8a	$⊢ (φ \land \exists y ψ) \to \exists x (φ \land \exists y ψ)$
13	9 11 12	syl56	$⊢ \neg \forall x x = y \to (\exists y (φ \land ψ) \to \exists x (φ \land \exists y ψ))$
14	8 13	pm2.61i	$⊢ \exists y (φ \land ψ) \to \exists x (φ \land \exists y ψ)$
15	2 14	exlimi	$⊢ \exists x \exists y (φ \land ψ) \to \exists x (φ \land \exists y ψ)$

Metamath Proof Explorer

Theorem exdistrf

Proof