Metamath Proof Explorer

Theorem nfra2wOLD

Description: Obsolete version of nfra2w as of 31-Oct-2024. (Contributed by Alan Sare, 31-Dec-2011) (Revised by GG, 24-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nfra2wOLD 
|- F/ y A. x e. A A. y e. B ph

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A A. y e. B ph <-> A. x ( x e. A -> A. y e. B ph ) )
2 df-ral 
 |-  ( A. y e. B ph <-> A. y ( y e. B -> ph ) )
3 2 imbi2i 
 |-  ( ( x e. A -> A. y e. B ph ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
4 3 albii 
 |-  ( A. x ( x e. A -> A. y e. B ph ) <-> A. x ( x e. A -> A. y ( y e. B -> ph ) ) )
5 1 4 bitri 
 |-  ( A. x e. A A. y e. B ph <-> A. x ( x e. A -> A. y ( y e. B -> ph ) ) )
6 nfa1 
 |-  F/ y A. y A. x ( x e. A -> ( y e. B -> ph ) )
7 alcom 
 |-  ( A. y A. x ( x e. A -> ( y e. B -> ph ) ) <-> A. x A. y ( x e. A -> ( y e. B -> ph ) ) )
8 19.21v 
 |-  ( A. y ( x e. A -> ( y e. B -> ph ) ) <-> ( x e. A -> A. y ( y e. B -> ph ) ) )
9 8 albii 
 |-  ( A. x A. y ( x e. A -> ( y e. B -> ph ) ) <-> A. x ( x e. A -> A. y ( y e. B -> ph ) ) )
10 7 9 bitri 
 |-  ( A. y A. x ( x e. A -> ( y e. B -> ph ) ) <-> A. x ( x e. A -> A. y ( y e. B -> ph ) ) )
11 10 nfbii 
 |-  ( F/ y A. y A. x ( x e. A -> ( y e. B -> ph ) ) <-> F/ y A. x ( x e. A -> A. y ( y e. B -> ph ) ) )
12 6 11 mpbi 
 |-  F/ y A. x ( x e. A -> A. y ( y e. B -> ph ) )
13 5 12 nfxfr 
 |-  F/ y A. x e. A A. y e. B ph