Theorem 2sb6rf

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 variable constraints. (Revised by Wolf Lammen, 28-Sep-2018) (Proof shortened by Wolf Lammen, 13-Apr-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2sb5rf.1	|- F/ z ph
	2sb5rf.2	|- F/ w ph
Assertion	2sb6rf	|- ( ph <-> A. z A. 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.23	|- ( A. z ( E. w ( z = x /\ w = y ) -> ph ) <-> ( E. z E. w ( z = x /\ w = y ) -> ph ) )
4	2	19.23	|- ( A. w ( ( z = x /\ w = y ) -> ph ) <-> ( E. w ( z = x /\ w = y ) -> ph ) )
5	4	albii	|- ( A. z A. w ( ( z = x /\ w = y ) -> ph ) <-> A. z ( E. w ( z = x /\ w = y ) -> ph ) )
6		2ax6e	|- E. z E. w ( z = x /\ w = y )
7	6	a1bi	|- ( ph <-> ( E. z E. w ( z = x /\ w = y ) -> ph ) )
8	3 5 7	3bitr4ri	|- ( ph <-> A. z A. 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.74i	|- ( ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) <-> ( ( z = x /\ w = y ) -> ph ) )
13	12	2albii	|- ( A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) <-> A. z A. w ( ( z = x /\ w = y ) -> ph ) )
14	8 13	bitr4i	|- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )