Theorem 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 ). Usage of this theorem is discouraged because it depends on ax-13 . Check out exdistr for a version requiring fewer axioms. (Contributed by Mario Carneiro, 20-Mar-2013) (Proof shortened by Wolf Lammen, 14-May-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	exdistrf.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 )
Assertion	exdistrf	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrf.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 )
2		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 )
3		19.8a	⊢ ( 𝜓 → ∃ 𝑦 𝜓 )
4	3	anim2i	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )
5	4	eximi	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑦 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )
6		biidd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
7	6	drex1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ↔ ∃ 𝑦 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
8	5 7	syl5ibr	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
9		19.40	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑦 𝜑 ∧ ∃ 𝑦 𝜓 ) )
10	1	19.9d	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 𝜑 → 𝜑 ) )
11	10	anim1d	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑦 𝜑 ∧ ∃ 𝑦 𝜓 ) → ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
12		19.8a	⊢ ( ( 𝜑 ∧ ∃ 𝑦 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )
13	9 11 12	syl56	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
14	8 13	pm2.61i	⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )
15	2 14	exlimi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )