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 1936 | . 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) | |
2 | 1 | r2allem 3200 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1531 ∈ wcel 2110 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-ral 3143 |
This theorem is referenced by: r3al 3202 r2ex 3303 ralcom 3354 raliunxp 5704 codir 5974 qfto 5975 fununi 6423 dff13 7007 mpo2eqb 7277 tz7.48lem 8071 qliftfun 8376 zorn2lem4 9915 isirred2 19445 cnmpt12 22269 cnmpt22 22276 dchrelbas3 25808 cvmlift2lem12 32556 dfso2 32985 dfpo2 32986 inxpss 35563 inxpss3 35565 isdomn3 39797 |
Copyright terms: Public domain | W3C validator |