This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ). (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 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝜑 )
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 imbitrrid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) ) )
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 ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )