![]() |
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.) |
Ref | Expression |
---|---|
rexcom | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2968 | . 2 ⊢ Ⅎ𝑦𝐴 | |
2 | nfcv 2968 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | rexcomf 3306 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∃wrex 3117 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 |
This theorem is referenced by: rexcom13 3310 rexcom4 3441 iuncom 4746 xpiundi 5405 brdom7disj 9667 addcompr 10157 mulcompr 10159 qmulz 12073 elpq 12096 caubnd2 14473 ello1mpt2 14629 o1lo1 14644 lo1add 14733 lo1mul 14734 rlimno1 14760 sqrt2irr 15351 bezoutlem2 15629 bezoutlem4 15631 pythagtriplem19 15908 lsmcom2 18420 efgrelexlemb 18515 lsmcomx 18611 pgpfac1lem2 18827 pgpfac1lem4 18830 regsep2 21550 ordthaus 21558 tgcmp 21574 txcmplem1 21814 xkococnlem 21832 regr1lem2 21913 dyadmax 23763 coeeu 24379 ostth 25740 axpasch 26239 axeuclidlem 26260 usgr2pth0 27066 elwwlks2 27294 elwspths2spth 27295 shscom 28732 mdsymlem4 29819 mdsymlem8 29823 ordtconnlem1 30514 cvmliftlem15 31825 lshpsmreu 35183 islpln5 35609 islvol5 35653 paddcom 35887 mapdrvallem2 37719 hdmapglem7a 38001 fourierdlem42 41159 2rexsb 41995 2rexrsb 41996 2reurex 42005 2reu1 42010 2reu4a 42013 pgrpgt2nabl 42993 islindeps2 43118 isldepslvec2 43120 |
Copyright terms: Public domain | W3C validator |