![]() |
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 1943 | . 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) | |
2 | 1 | r2allem 3136 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∀wal 1540 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3062 |
This theorem is referenced by: r2ex 3189 r3al 3190 ralcom 3271 nfra2w 3281 moel 3374 raliunxp 5796 codir 6075 qfto 6076 dfpo2 6249 fununi 6577 dff13 7203 mpo2eqb 7489 frpoins3xpg 8073 xpord2indlem 8080 tz7.48lem 8388 qliftfun 8744 zorn2lem4 10440 isirred2 20137 cnmpt12 23034 cnmpt22 23041 dchrelbas3 26602 cvmlift2lem12 33965 dfso2 34384 r2alan 36753 inxpss 36818 inxpss3 36821 isdomn3 41574 iscnrm3lem2 47053 joindm2 47087 meetdm2 47089 |
Copyright terms: Public domain | W3C validator |