![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexcom | Structured version Visualization version GIF version |
Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2024.) |
Ref | Expression |
---|---|
rexcom | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralcom 3271 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | ralnex2 3127 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | |
3 | ralnex2 3127 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | |
4 | 1, 2, 3 | 3bitr3i 301 | . 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
5 | 4 | con4bii 321 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wral 3061 ∃wrex 3070 |
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 ax-11 2155 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-ral 3062 df-rex 3071 |
This theorem is referenced by: rexcom13 3278 2reurex 3719 2reu1 3854 2reu4lem 4484 iuncom 4962 xpiundi 5703 brdom7disj 10472 addcompr 10962 mulcompr 10964 qmulz 12881 elpq 12905 caubnd2 15248 ello1mpt2 15410 o1lo1 15425 lo1add 15515 lo1mul 15516 rlimno1 15544 sqrt2irr 16136 bezoutlem2 16426 bezoutlem4 16428 pythagtriplem19 16710 lsmcom2 19442 efgrelexlemb 19537 lsmcomx 19639 pgpfac1lem2 19859 pgpfac1lem4 19862 regsep2 22743 ordthaus 22751 tgcmp 22768 txcmplem1 23008 xkococnlem 23026 regr1lem2 23107 dyadmax 24978 coeeu 25602 ostth 27003 axpasch 27932 axeuclidlem 27953 usgr2pth0 28755 elwwlks2 28953 elwspths2spth 28954 shscom 30303 mdsymlem4 31390 mdsymlem8 31394 ordtconnlem1 32562 cvmliftlem15 33949 fvineqsneq 35929 lshpsmreu 37617 islpln5 38044 islvol5 38088 paddcom 38322 mapdrvallem2 40154 hdmapglem7a 40436 fsuppind 40808 fourierdlem42 44476 2rexsb 45419 2rexrsb 45420 pgrpgt2nabl 46528 islindeps2 46650 isldepslvec2 46652 |
Copyright terms: Public domain | W3C validator |