Theorem 2sb5rf

Description: Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Feb-2005) (Revised by Mario Carneiro, 6-Oct-2016) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2sb5rf.1	|- F/ z ph
	2sb5rf.2	|- F/ w ph
Assertion	2sb5rf	|- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		2sb5rf.1	|- F/ z ph
2		2sb5rf.2	|- F/ w ph
3	1	19.41	|- ( E. z ( E. w ( z = x /\ w = y ) /\ ph ) <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
4	2	19.41	|- ( E. w ( ( z = x /\ w = y ) /\ ph ) <-> ( E. w ( z = x /\ w = y ) /\ ph ) )
5	4	exbii	|- ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> E. z ( E. w ( z = x /\ w = y ) /\ ph ) )
6		2ax6e	|- E. z E. w ( z = x /\ w = y )
7	6	biantrur	|- ( ph <-> ( E. z E. w ( z = x /\ w = y ) /\ ph ) )
8	3 5 7	3bitr4ri	|- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ ph ) )
9		sbequ12r	|- ( z = x -> ( [ z / x ] [ w / y ] ph <-> [ w / y ] ph ) )
10		sbequ12r	|- ( w = y -> ( [ w / y ] ph <-> ph ) )
11	9 10	sylan9bb	|- ( ( z = x /\ w = y ) -> ( [ z / x ] [ w / y ] ph <-> ph ) )
12	11	pm5.32i	|- ( ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) <-> ( ( z = x /\ w = y ) /\ ph ) )
13	12	2exbii	|- ( E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) <-> E. z E. w ( ( z = x /\ w = y ) /\ ph ) )
14	8 13	bitr4i	|- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )