![]() |
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 1935 | . 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) | |
2 | 1 | r2allem 3132 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1532 ∈ wcel 2099 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-ral 3052 |
This theorem is referenced by: r2ex 3186 r3al 3187 ralcom 3277 nfra2w 3287 moel 3386 raliunxp 5846 codir 6132 qfto 6133 dfpo2 6307 fununi 6634 dff13 7270 mpo2eqb 7558 frpoins3xpg 8154 xpord2indlem 8161 tz7.48lem 8471 qliftfun 8831 zorn2lem4 10542 isirred2 20403 isdomn3 20693 cnmpt12 23662 cnmpt22 23669 dchrelbas3 27267 cvmlift2lem12 35142 dfso2 35577 r2alan 37947 inxpss 38009 inxpss3 38012 iscnrm3lem2 48268 joindm2 48302 meetdm2 48304 |
Copyright terms: Public domain | W3C validator |