![]() |
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 2035 | . 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) | |
2 | 1 | r2allem 3117 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∀wal 1651 ∈ wcel 2157 ∀wral 3088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-ral 3093 |
This theorem is referenced by: r3al 3120 r2ex 3241 soss 5250 raliunxp 5464 codir 5733 qfto 5734 fununi 6174 dff13 6739 mpt22eqb 7002 tz7.48lem 7774 qliftfun 8069 zorn2lem4 9608 isirred2 19014 cnmpt12 21796 cnmpt22 21803 dchrelbas3 25312 cvmlift2lem12 31806 dfso2 32151 dfpo2 32152 inxpss 34570 inxpss3 34572 isdomn3 38556 |
Copyright terms: Public domain | W3C validator |