![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralcom | Structured version Visualization version GIF version |
Description: Commutation of restricted universal quantifiers. See ralcom2 3371 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3371 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
ralcom | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomst 463 | . . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
2 | 1 | 2albii 1814 | . . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) |
3 | alcom 2148 | . . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
4 | 2, 3 | bitri 274 | . 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) |
5 | r2al 3192 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | |
6 | r2al 3192 | . 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑)) | |
7 | 4, 5, 6 | 3bitr4i 302 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 ∈ wcel 2098 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-11 2146 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-ral 3059 |
This theorem is referenced by: rexcom 3285 ralrot3 3288 ralcom13 3289 ralcom13OLD 3290 2reu4lem 4529 ssint 4971 iinrab2 5077 disjxun 5150 reusv3 5409 cnvpo 6296 cnvso 6297 dfpo2 6305 fununi 6633 isocnv2 7345 dfsmo2 8374 tz7.48lem 8468 ixpiin 8949 boxriin 8965 dedekind 11415 rexfiuz 15334 gcdcllem1 16481 mreacs 17645 comfeq 17693 catpropd 17696 isnsg2 19118 cntzrec 19294 oppgsubm 19323 opprirred 20368 opprsubrng 20503 opprsubrg 20539 rmodislmodlem 20819 rmodislmod 20820 rmodislmodOLD 20821 islindf4 21779 cpmatmcllem 22640 tgss2 22910 ist1-2 23271 kgencn 23480 ptcnplem 23545 cnmptcom 23602 fbun 23764 cnflf 23926 fclsopn 23938 cnfcf 23966 isclmp 25044 isncvsngp 25097 caucfil 25231 ovolgelb 25429 dyadmax 25547 ftc1a 25992 ulmcau 26351 noetasuplem4 27689 conway 27752 cofcutr 27864 addsprop 27913 perpcom 28537 colinearalg 28741 uhgrvd00 29368 pthdlem2lem 29601 frgrwopregbsn 30147 phoeqi 30687 ho02i 31659 hoeq2 31661 adjsym 31663 cnvadj 31722 mddmd2 32139 cdj3lem3b 32270 mgccnv 32747 cvmlift2lem12 34957 elpotr 35410 fvineqsnf1 36922 poimirlem29 37155 heicant 37161 ispsubsp2 39251 fsuppind 41854 nla0003 42886 ntrclsiso 43528 ntrneiiso 43552 ntrneik2 43553 ntrneix2 43554 ntrneik3 43557 ntrneix3 43558 ntrneik13 43559 ntrneix13 43560 ntrneik4w 43561 imo72b2 43633 tratrb 44006 hbra2VD 44330 tratrbVD 44331 |
Copyright terms: Public domain | W3C validator |