Theorem ralidmOLD

Description: Obsolete version of ralidm as of 2-Sep-2024. (Contributed by NM, 28-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ralidmOLD	|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		rzal	|- ( A = (/) -> A. x e. A A. x e. A ph )
2		rzal	|- ( A = (/) -> A. x e. A ph )
3	1 2	2thd	|- ( A = (/) -> ( A. x e. A A. x e. A ph <-> A. x e. A ph ) )
4		neq0	|- ( -. A = (/) <-> E. x x e. A )
5		df-ral	|- ( A. x e. A A. x e. A ph <-> A. x ( x e. A -> A. x e. A ph ) )
6		nfra1	|- F/ x A. x e. A ph
7	6	19.23	|- ( A. x ( x e. A -> A. x e. A ph ) <-> ( E. x x e. A -> A. x e. A ph ) )
8	5 7	bitri	|- ( A. x e. A A. x e. A ph <-> ( E. x x e. A -> A. x e. A ph ) )
9		biimt	|- ( E. x x e. A -> ( A. x e. A ph <-> ( E. x x e. A -> A. x e. A ph ) ) )
10	8 9	bitr4id	|- ( E. x x e. A -> ( A. x e. A A. x e. A ph <-> A. x e. A ph ) )
11	4 10	sylbi	|- ( -. A = (/) -> ( A. x e. A A. x e. A ph <-> A. x e. A ph ) )
12	3 11	pm2.61i	|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )