Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralcom4 | Structured version Visualization version GIF version |
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) |
Ref | Expression |
---|---|
ralcom4 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralcom 3079 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥 ∈ 𝐴 𝜑) | |
2 | ralv 3192 | . . 3 ⊢ (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑) | |
3 | 2 | ralbii 2963 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ V 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦𝜑) |
4 | ralv 3192 | . 2 ⊢ (∀𝑦 ∈ V ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) | |
5 | 1, 3, 4 | 3bitr3i 289 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 ∀wral 2896 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 |
This theorem is referenced by: ralxpxfr2d 3298 uniiunlem 3653 iunss 4497 disjor 4567 trint 4696 reliun 5162 funimass4 6157 ralrnmpt2 6673 findcard3 8088 kmlem12 8866 fimaxre3 10849 vdwmc2 15521 ramtlecl 15542 iunocv 19844 1stccn 21076 itg2leub 23307 mptelee 25575 nmoubi 27011 nmopub 28151 nmfnleub 28168 moel 28707 disjorf 28774 funcnv5mpt 28852 untuni 30840 heibor1lem 32778 pmapglbx 34073 ss2iundf 36970 iunssf 38290 setrec1lem2 42234 |
Copyright terms: Public domain | W3C validator |