| 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 3289 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
| 2 | ralnex2 3133 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | |
| 3 | ralnex2 3133 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) | |
| 4 | 1, 2, 3 | 3bitr3i 301 | . 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
| 5 | 4 | con4bii 321 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wral 3061 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-11 2157 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: rexcom13 3296 2reurex 3766 2reu1 3897 2reu4lem 4522 iuncom 4999 xpiundi 5756 brdom7disj 10571 addcompr 11061 mulcompr 11063 qmulz 12993 elpq 13017 caubnd2 15396 ello1mpt2 15558 o1lo1 15573 lo1add 15663 lo1mul 15664 rlimno1 15690 sqrt2irr 16285 bezoutlem2 16577 bezoutlem4 16579 pythagtriplem19 16871 lsmcom2 19673 efgrelexlemb 19768 lsmcomx 19874 pgpfac1lem2 20095 pgpfac1lem4 20098 regsep2 23384 ordthaus 23392 tgcmp 23409 txcmplem1 23649 xkococnlem 23667 regr1lem2 23748 dyadmax 25633 coeeu 26264 ostth 27683 mulscom 28165 znegscl 28378 axpasch 28956 axeuclidlem 28977 usgr2pth0 29785 elwwlks2 29986 elwspths2spth 29987 shscom 31338 mdsymlem4 32425 mdsymlem8 32429 ordtconnlem1 33923 cvmliftlem15 35303 fvineqsneq 37413 lshpsmreu 39110 islpln5 39537 islvol5 39581 paddcom 39815 mapdrvallem2 41647 hdmapglem7a 41929 remexz 42105 hashnexinjle 42130 fimgmcyclem 42543 fsuppind 42600 fourierdlem42 46164 2rexsb 47113 2rexrsb 47114 pgrpgt2nabl 48282 islindeps2 48400 isldepslvec2 48402 |
| Copyright terms: Public domain | W3C validator |