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 ⊢ ¬ ∀ x x = y → Ⅎ y φ
Assertion exdistrf ⊢ ∃ x ∃ y φ ∧ ψ → ∃ x φ ∧ ∃ y ψ

Proof

Step Hyp Ref Expression
1 exdistrf.1 ⊢ ¬ ∀ x x = y → Ⅎ y φ
2 nfe1 ⊢ Ⅎ x ∃ x φ ∧ ∃ y ψ
3 19.8a ⊢ ψ → ∃ y ψ
4 3 anim2i ⊢ φ ∧ ψ → φ ∧ ∃ y ψ
5 4 eximi ⊢ ∃ y φ ∧ ψ → ∃ y φ ∧ ∃ y ψ
6 biidd ⊢ ∀ x x = y → φ ∧ ∃ y ψ ↔ φ ∧ ∃ y ψ
7 6 drex1 ⊢ ∀ x x = y → ∃ x φ ∧ ∃ y ψ ↔ ∃ y φ ∧ ∃ y ψ
8 5 7 imbitrrid ⊢ ∀ x x = y → ∃ y φ ∧ ψ → ∃ x φ ∧ ∃ y ψ
9 19.40 ⊢ ∃ y φ ∧ ψ → ∃ y φ ∧ ∃ y ψ
10 1 19.9d ⊢ ¬ ∀ x x = y → ∃ y φ → φ
11 10 anim1d ⊢ ¬ ∀ x x = y → ∃ y φ ∧ ∃ y ψ → φ ∧ ∃ y ψ
12 19.8a ⊢ φ ∧ ∃ y ψ → ∃ x φ ∧ ∃ y ψ
13 9 11 12 syl56 ⊢ ¬ ∀ x x = y → ∃ y φ ∧ ψ → ∃ x φ ∧ ∃ y ψ
14 8 13 pm2.61i ⊢ ∃ y φ ∧ ψ → ∃ x φ ∧ ∃ y ψ
15 2 14 exlimi ⊢ ∃ x ∃ y φ ∧ ψ → ∃ x φ ∧ ∃ y ψ