Theorem sbel2x

Description: Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 5-Aug-1993) (Proof shortened by Wolf Lammen, 29-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	sbel2x	|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ph
2		nfv	|- F/ x ph
3	1 2	2sb5rf	|- ( ph <-> E. y E. x ( ( y = w /\ x = z ) /\ [ y / w ] [ x / z ] ph ) )
4		ancom	|- ( ( y = w /\ x = z ) <-> ( x = z /\ y = w ) )
5	4	anbi1i	|- ( ( ( y = w /\ x = z ) /\ [ y / w ] [ x / z ] ph ) <-> ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
6	5	2exbii	|- ( E. y E. x ( ( y = w /\ x = z ) /\ [ y / w ] [ x / z ] ph ) <-> E. y E. x ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
7		excom	|- ( E. y E. x ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
8	3 6 7	3bitri	|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )