Metamath Proof Explorer

Theorem ralcom2

Description: Commutation of restricted universal quantifiers. Note that x and y need not be disjoint (this makes the proof longer). This theorem relies on the full set of axioms up to ax-ext and it should no longer be used. Usage of ralcom is highly encouraged. (Contributed by NM, 24-Nov-1994) (Proof shortened by Mario Carneiro, 17-Oct-2016) (New usage is discouraged.)

Ref Expression
Assertion ralcom2 
|- ( A. x e. A A. y e. A ph -> A. y e. A A. x e. A ph )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
2 1 sps 
 |-  ( A. x x = y -> ( x e. A <-> y e. A ) )
3 2 imbi1d 
 |-  ( A. x x = y -> ( ( x e. A -> ph ) <-> ( y e. A -> ph ) ) )
4 3 dral1 
 |-  ( A. x x = y -> ( A. x ( x e. A -> ph ) <-> A. y ( y e. A -> ph ) ) )
5 4 bicomd 
 |-  ( A. x x = y -> ( A. y ( y e. A -> ph ) <-> A. x ( x e. A -> ph ) ) )
6 df-ral 
 |-  ( A. y e. A ph <-> A. y ( y e. A -> ph ) )
7 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
8 5 6 7 3bitr4g 
 |-  ( A. x x = y -> ( A. y e. A ph <-> A. x e. A ph ) )
9 2 8 imbi12d 
 |-  ( A. x x = y -> ( ( x e. A -> A. y e. A ph ) <-> ( y e. A -> A. x e. A ph ) ) )
10 9 dral1 
 |-  ( A. x x = y -> ( A. x ( x e. A -> A. y e. A ph ) <-> A. y ( y e. A -> A. x e. A ph ) ) )
11 df-ral 
 |-  ( A. x e. A A. y e. A ph <-> A. x ( x e. A -> A. y e. A ph ) )
12 df-ral 
 |-  ( A. y e. A A. x e. A ph <-> A. y ( y e. A -> A. x e. A ph ) )
13 10 11 12 3bitr4g 
 |-  ( A. x x = y -> ( A. x e. A A. y e. A ph <-> A. y e. A A. x e. A ph ) )
14 13 biimpd 
 |-  ( A. x x = y -> ( A. x e. A A. y e. A ph -> A. y e. A A. x e. A ph ) )
15 nfnae 
 |-  F/ y -. A. x x = y
16 nfra2 
 |-  F/ y A. x e. A A. y e. A ph
17 15 16 nfan 
 |-  F/ y ( -. A. x x = y /\ A. x e. A A. y e. A ph )
18 nfnae 
 |-  F/ x -. A. x x = y
19 nfra1 
 |-  F/ x A. x e. A A. y e. A ph
20 18 19 nfan 
 |-  F/ x ( -. A. x x = y /\ A. x e. A A. y e. A ph )
21 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
22 21 adantr 
 |-  ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) -> F/_ x y )
23 nfcvd 
 |-  ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) -> F/_ x A )
24 22 23 nfeld 
 |-  ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) -> F/ x y e. A )
25 20 24 nfan1 
 |-  F/ x ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) /\ y e. A )
26 rsp2 
 |-  ( A. x e. A A. y e. A ph -> ( ( x e. A /\ y e. A ) -> ph ) )
27 26 ancomsd 
 |-  ( A. x e. A A. y e. A ph -> ( ( y e. A /\ x e. A ) -> ph ) )
28 27 expdimp 
 |-  ( ( A. x e. A A. y e. A ph /\ y e. A ) -> ( x e. A -> ph ) )
29 28 adantll 
 |-  ( ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) /\ y e. A ) -> ( x e. A -> ph ) )
30 25 29 ralrimi 
 |-  ( ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) /\ y e. A ) -> A. x e. A ph )
31 30 ex 
 |-  ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) -> ( y e. A -> A. x e. A ph ) )
32 17 31 ralrimi 
 |-  ( ( -. A. x x = y /\ A. x e. A A. y e. A ph ) -> A. y e. A A. x e. A ph )
33 32 ex 
 |-  ( -. A. x x = y -> ( A. x e. A A. y e. A ph -> A. y e. A A. x e. A ph ) )
34 14 33 pm2.61i 
 |-  ( A. x e. A A. y e. A ph -> A. y e. A A. x e. A ph )