Metamath Proof Explorer


Theorem exisym1

Description: A symmetry with E. .

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

Ref Expression
Assertion exisym1
|- ( E. x E. x F. -> E. x ph )

Proof

Step Hyp Ref Expression
1 nfe1
 |-  F/ x E. x ph
2 falim
 |-  ( F. -> ph )
3 2 eximi
 |-  ( E. x F. -> E. x ph )
4 1 3 exlimi
 |-  ( E. x E. x F. -> E. x ph )