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 2751 | . 2 ⊢ Ⅎ𝑦𝐴 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | rexcomf 3078 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 |
This theorem is referenced by: rexcom13 3081 rexcom4 3198 iuncom 4463 xpiundi 5096 brdom7disj 9234 addcompr 9722 mulcompr 9724 qmulz 11667 caubnd2 13945 ello1mpt2 14101 o1lo1 14116 lo1add 14205 lo1mul 14206 rlimno1 14232 sqrt2irr 14817 bezoutlem2 15095 bezoutlem4 15097 pythagtriplem19 15376 lsmcom2 17893 efgrelexlemb 17986 lsmcomx 18082 pgpfac1lem2 18297 pgpfac1lem4 18300 regsep2 20990 ordthaus 20998 tgcmp 21014 txcmplem1 21254 xkococnlem 21272 regr1lem2 21353 dyadmax 23172 coeeu 23785 ostth 25128 axpasch 25621 axeuclidlem 25642 el2wlksot 26407 el2pthsot 26408 frgrawopreglem5 26575 shscom 27562 mdsymlem4 28649 mdsymlem8 28653 ordtconlem1 29298 cvmliftlem15 30534 nofulllem5 31105 lshpsmreu 33414 islpln5 33839 islvol5 33883 paddcom 34117 mapdrvallem2 35952 hdmapglem7a 36237 fourierdlem42 39042 2rexsb 39819 2rexrsb 39820 2reurex 39830 2reu1 39835 2reu4a 39838 usgr2pth0 40971 elwwlks2 41170 elwspths2spth 41171 frgrwopreglem5 41485 pgrpgt2nabl 41941 islindeps2 42066 isldepslvec2 42068 |
Copyright terms: Public domain | W3C validator |