This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralidm

Description: Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997) Reduce axiom usage. (Revised by GG, 2-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A A. x e. A ph <-> A. x ( x e. A -> A. x e. A ph ) )
2 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3 ax-1 
 |-  ( A. x ( x e. A -> ph ) -> ( x e. A -> A. x ( x e. A -> ph ) ) )
4 3 axc4i 
 |-  ( A. x ( x e. A -> ph ) -> A. x ( x e. A -> A. x ( x e. A -> ph ) ) )
5 pm2.21 
 |-  ( -. x e. A -> ( x e. A -> ph ) )
6 sp 
 |-  ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
7 5 6 ja 
 |-  ( ( x e. A -> A. x ( x e. A -> ph ) ) -> ( x e. A -> ph ) )
8 7 alimi 
 |-  ( A. x ( x e. A -> A. x ( x e. A -> ph ) ) -> A. x ( x e. A -> ph ) )
9 4 8 impbii 
 |-  ( A. x ( x e. A -> ph ) <-> A. x ( x e. A -> A. x ( x e. A -> ph ) ) )
10 2 bicomi 
 |-  ( A. x ( x e. A -> ph ) <-> A. x e. A ph )
11 10 imbi2i 
 |-  ( ( x e. A -> A. x ( x e. A -> ph ) ) <-> ( x e. A -> A. x e. A ph ) )
12 11 albii 
 |-  ( A. x ( x e. A -> A. x ( x e. A -> ph ) ) <-> A. x ( x e. A -> A. x e. A ph ) )
13 2 9 12 3bitrri 
 |-  ( A. x ( x e. A -> A. x e. A ph ) <-> A. x e. A ph )
14 1 13 bitri 
 |-  ( A. x e. A A. x e. A ph <-> A. x e. A ph )