Theorem 19.12vv

Description: Special case of 19.12 where its converse holds. See 19.12vvv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 18-Jul-2001) (Revised by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	19.12vv	|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.21v	|- ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) )
2	1	exbii	|- ( E. x A. y ( ph -> ps ) <-> E. x ( ph -> A. y ps ) )
3		nfv	|- F/ x ps
4	3	nfal	|- F/ x A. y ps
5	4	19.36	|- ( E. x ( ph -> A. y ps ) <-> ( A. x ph -> A. y ps ) )
6		19.36v	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
7	6	albii	|- ( A. y E. x ( ph -> ps ) <-> A. y ( A. x ph -> ps ) )
8		nfv	|- F/ y ph
9	8	nfal	|- F/ y A. x ph
10	9	19.21	|- ( A. y ( A. x ph -> ps ) <-> ( A. x ph -> A. y ps ) )
11	7 10	bitr2i	|- ( ( A. x ph -> A. y ps ) <-> A. y E. x ( ph -> ps ) )
12	2 5 11	3bitri	|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )