Theorem subsym1

Description: A symmetry with [ x / y ] .

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

	Ref	Expression
Assertion	subsym1	|- ( [ y / x ] [ y / x ] F. -> [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		fal	|- -. F.
2	1	intnan	|- -. ( x = y /\ F. )
3	2	nex	|- -. E. x ( x = y /\ F. )
4	3	intnan	|- -. ( ( x = y -> F. ) /\ E. x ( x = y /\ F. ) )
5		dfsb1	|- ( [ y / x ] F. <-> ( ( x = y -> F. ) /\ E. x ( x = y /\ F. ) ) )
6	4 5	mtbir	|- -. [ y / x ] F.
7	6	intnan	|- -. ( x = y /\ [ y / x ] F. )
8	7	nex	|- -. E. x ( x = y /\ [ y / x ] F. )
9	8	intnan	|- -. ( ( x = y -> [ y / x ] F. ) /\ E. x ( x = y /\ [ y / x ] F. ) )
10		dfsb1	|- ( [ y / x ] [ y / x ] F. <-> ( ( x = y -> [ y / x ] F. ) /\ E. x ( x = y /\ [ y / x ] F. ) ) )
11	9 10	mtbir	|- -. [ y / x ] [ y / x ] F.
12	11	pm2.21i	|- ( [ y / x ] [ y / x ] F. -> [ y / x ] ph )