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 ). 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 ¬ 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 syl5ibr 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 ψ