Metamath Proof Explorer


Theorem amosym1

Description: A symmetry with E* .

See negsym1 for more information. (Contributed by Anthony Hart, 13-Sep-2011)

Ref Expression
Assertion amosym1 * x * x * x φ

Proof

Step Hyp Ref Expression
1 moeu * x * x x * x ∃! x * x
2 mofal * x
3 19.8a * x x * x
4 3 notnotd * x ¬ ¬ x * x
5 2 4 ax-mp ¬ ¬ x * x
6 5 pm2.21i ¬ x * x * x φ
7 2 notnoti ¬ ¬ * x
8 7 nex ¬ x ¬ * x
9 eunex ∃! x * x x ¬ * x
10 8 9 mto ¬ ∃! x * x
11 10 pm2.21i ∃! x * x * x φ
12 6 11 ja x * x ∃! x * x * x φ
13 1 12 sylbi * x * x * x φ