Metamath Proof Explorer

Theorem nfra2wOLD

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

Ref Expression
Assertion nfra2wOLD ⊢Ⅎy∀x∈A∀y∈Bφ

Proof

Step Hyp Ref Expression
1 df-ral ⊢∀x∈A∀y∈Bφ↔∀xx∈A→∀y∈Bφ
2 df-ral ⊢∀y∈Bφ↔∀yy∈B→φ
3 2 imbi2i ⊢x∈A→∀y∈Bφ↔x∈A→∀yy∈B→φ
4 3 albii ⊢∀xx∈A→∀y∈Bφ↔∀xx∈A→∀yy∈B→φ
5 1 4 bitri ⊢∀x∈A∀y∈Bφ↔∀xx∈A→∀yy∈B→φ
6 nfa1 ⊢Ⅎy∀y∀xx∈A→y∈B→φ
7 alcom ⊢∀y∀xx∈A→y∈B→φ↔∀x∀yx∈A→y∈B→φ
8 19.21v ⊢∀yx∈A→y∈B→φ↔x∈A→∀yy∈B→φ
9 8 albii ⊢∀x∀yx∈A→y∈B→φ↔∀xx∈A→∀yy∈B→φ
10 7 9 bitri ⊢∀y∀xx∈A→y∈B→φ↔∀xx∈A→∀yy∈B→φ
11 10 nfbii ⊢Ⅎy∀y∀xx∈A→y∈B→φ↔Ⅎy∀xx∈A→∀yy∈B→φ
12 6 11 mpbi ⊢Ⅎy∀xx∈A→∀yy∈B→φ
13 5 12 nfxfr ⊢Ⅎy∀x∈A∀y∈Bφ