![]() |
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 3276 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | ralnex2 3122 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | |
3 | ralnex2 3122 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | |
4 | 1, 2, 3 | 3bitr3i 300 | . 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
5 | 4 | con4bii 320 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wral 3050 ∃wrex 3059 |
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 3051 df-rex 3060 |
This theorem is referenced by: rexcom13 3283 2reurex 3752 2reu1 3887 2reu4lem 4527 iuncom 5004 xpiundi 5748 brdom7disj 10556 addcompr 11046 mulcompr 11048 qmulz 12968 elpq 12992 caubnd2 15340 ello1mpt2 15502 o1lo1 15517 lo1add 15607 lo1mul 15608 rlimno1 15636 sqrt2irr 16229 bezoutlem2 16519 bezoutlem4 16521 pythagtriplem19 16805 lsmcom2 19622 efgrelexlemb 19717 lsmcomx 19823 pgpfac1lem2 20044 pgpfac1lem4 20047 regsep2 23324 ordthaus 23332 tgcmp 23349 txcmplem1 23589 xkococnlem 23607 regr1lem2 23688 dyadmax 25571 coeeu 26204 ostth 27617 mulscom 28089 znegscl 28289 axpasch 28824 axeuclidlem 28845 usgr2pth0 29651 elwwlks2 29849 elwspths2spth 29850 shscom 31201 mdsymlem4 32288 mdsymlem8 32292 ordtconnlem1 33656 cvmliftlem15 35039 fvineqsneq 37022 lshpsmreu 38711 islpln5 39138 islvol5 39182 paddcom 39416 mapdrvallem2 41248 hdmapglem7a 41530 remexz 41707 hashnexinjle 41732 fsuppind 41958 fourierdlem42 45675 2rexsb 46619 2rexrsb 46620 pgrpgt2nabl 47616 islindeps2 47737 isldepslvec2 47739 |
Copyright terms: Public domain | W3C validator |