|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > r2al | Structured version Visualization version GIF version | ||
| Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.) | 
| Ref | Expression | 
|---|---|
| r2al | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 19.21v 1939 | . 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) | |
| 2 | 1 | r2allem 3142 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 | 
| This theorem is referenced by: r2ex 3196 r3al 3197 ralcom 3289 nfra2w 3299 moel 3402 raliunxp 5850 codir 6140 qfto 6141 dfpo2 6316 fununi 6641 dff13 7275 mpo2eqb 7565 frpoins3xpg 8165 xpord2indlem 8172 tz7.48lem 8481 qliftfun 8842 zorn2lem4 10539 isirred2 20421 isdomn3 20715 cnmpt12 23675 cnmpt22 23682 dchrelbas3 27282 cvmlift2lem12 35319 dfso2 35755 r2alan 38250 inxpss 38312 inxpss3 38315 dfac5prim 45007 iscnrm3lem2 48832 joindm2 48865 meetdm2 48867 | 
| Copyright terms: Public domain | W3C validator |